} == {eq:(T
T
)| 
x,y:T. 
(eq(x,y)) 
x = y }T:Type. {T=} 
Type
T == x:S. x Tb == if b
True else False fib:. b Prop Q == (P 
Q) & (P Q)A,B:Prop. (A B) Prop Q == Q PA,B:Prop. (A B) Prop| Who Cites discrete equality? | |
| discrete_equality | Def {T=} == {eq:(TT)| x,y:T. (eq(x,y)) x = y } |
| Thm* T:Type. {T=} Type | |
| subtype | Def S T == x:S. x T |
| assert | Def b == if b True else False fi |
| Thm* b:. b Prop | |
| iff | Def P Q == (P Q) & (P Q) |
| Thm* A,B:Prop. (A B) Prop | |
| rev_implies | Def P Q == Q P |
| Thm* A,B:Prop. (A B) Prop |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |  |