lean2/tests/lean/let2.lean.expected.out

13 lines
433 B
Text
Raw Normal View History

Set: pp::colors
Set: pp::unicode
Proved: simple
Theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r :=
Discharge
(λ H_pq_qr : (p ⇒ q) ∧ (q ⇒ r),
Discharge
(λ H_p : p,
let P_pq : p ⇒ q := Conjunct1 H_pq_qr,
P_qr : q ⇒ r := Conjunct2 H_pq_qr,
P_q : q := MP P_pq H_p
in MP P_qr P_q))