b == if b
True else False fi
Thm* 
b:
. b 
Prop
a:T. E(a;a)
Thm* T:Type, E:(T
TProp). Refl(T;x,y.E(x,y)) Prop
to a Prop is normally invisible since it is pretty obvious when it is
needed.
| assert |
Def b == if b True else False fi
Thm* |
| refl |
Def Refl(T;x,y.E(x;y)) == a:T. E(a;a)
Thm* |
About:
 |  |  |  |  |  |
 |  |  |  |  |