a:T. E(a;a)T:Type, E:(T
TProp). Refl(T;x,y.E(x,y)) 
Prop| NOTE: | Refl(A)(R(_1;_2)) is | alpha-equivalent | to Refl(A;x,y.R(x;y)). |
| Who Cites refl? | |
| refl | Def Refl(T;x,y.E(x;y)) == a:T. E(a;a) |
| Thm* T:Type, E:(TTProp). Refl(T;x,y.E(x,y)) Prop |
| Syntax: | Refl(T;x,y.E(x;y)) | has structure: | refl(T; x,y.E(x;y)) |
About:
 |  |  |  |  |  |