2. t: u Term
3. x: u
(t 
= x) 
Prop2. t: u Term
u Type (u Term) Type Type{i} Type{i'}
u:Type, t:(u Term), x:u. (t = x) Prop
| 1 | 1. u: Type 2. t: u Term 3. x: u (t = x) Prop | 3 steps |
| 2 | 1. u: Type 2. t: u Term u Type | Auto |
| 3 | 1. u: Type (u Term) Type | Auto |
| 4 | Type{i} Type{i'} | Auto |
About:
 |  |  |  |