lean2/tests/lean/run/using_bug.lean

9 lines
270 B
Text

example (p q r : Prop) : p ∧ q ∧ r → q ∧ p :=
assume Hpqr : p ∧ q ∧ r,
have Hp : p, from and.elim_left Hpqr,
have Hqr : q ∧ r, from and.elim_right Hpqr,
have Hq : q, from and.elim_left Hqr,
show q ∧ p, from
proof
and.intro Hq Hp
qed