} == {eq:(T
T
)| 
x,y:T. 
(eq(x,y)) 
x = y }
Thm* T:Type. {T=} 
Type
b == if b
True else False fi
Thm* b:. b Prop
Q == (P 
Q) & (P Q)
Thm* A,B:Prop. (A B) Prop
Q == Q P
Thm* A,B:Prop. (A B) Prop
| discrete_equality |
Def {T=} == {eq:(TT)| x,y:T. (eq(x,y)) x = y }
Thm* |
| assert |
Def b == if b True else False fi
Thm* |
| iff |
Def P Q == (P Q) & (P Q)
Thm* |
| rev_implies |
Def P Q == Q P
Thm* |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |