2. t: u Term
3. x: u
(t reps x 
u) Prop2. t: u Term
u Type (u Term) Type Type{i} Type{i'}
u:Type, t:(u Term), x:u. (t reps x u) Prop
| 1 | 1. u: Type 2. t: u Term 3. x: u (t reps x u) 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:
 |  |  |  |