} == {eq:(T
T
)| 
x,y:T. 
(eq(x,y)) 
x = y }T:Type. {T=} 
Typeb == 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 | |
| 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 |
| Syntax: | {T=} | has structure: | discrete_equality(T) |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |
 |