2013-09-02 12:29:21 -07:00
|
|
|
|
Set: pp::colors
|
2013-09-03 10:44:51 -07:00
|
|
|
|
Set: pp::unicode
|
2013-08-31 19:15:48 -07:00
|
|
|
|
Assumed: a
|
|
|
|
|
Assumed: b
|
|
|
|
|
a ∧ b
|
|
|
|
|
a ∧ b ∧ a
|
|
|
|
|
a ∧ b
|
|
|
|
|
a ∧ b
|
|
|
|
|
a ∧ b
|
|
|
|
|
a ∧ b
|
|
|
|
|
a ∨ b
|
|
|
|
|
a ∨ b
|
|
|
|
|
a ∨ b
|
|
|
|
|
a ∨ b
|
|
|
|
|
a ∨ a ∨ b
|
|
|
|
|
a ⇒ b ⇒ a
|
|
|
|
|
Bool
|
|
|
|
|
ite Bool a a ⊤
|
|
|
|
|
a
|
|
|
|
|
Assumed: H1
|
|
|
|
|
Assumed: H2
|
2013-09-01 10:34:57 -07:00
|
|
|
|
Π (a b : Bool) (H1 : a ⇒ b) (H2 : a), b
|
2013-08-31 19:15:48 -07:00
|
|
|
|
MP H2 H1
|
|
|
|
|
b
|