Prop2. tr: Term
3. L: Term
Prop
RepsTruth(L; Tr; tr) 
PropProp{i}2. tr: Term
TermProp{i} Type{i'}Prop Term Type TermProp{i} Type{i'}
Tr:(TermProp), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr) Prop
| 1 | 1. Tr: TermProp 2. tr: Term 3. L: Term Prop RepsTruth(L; Tr; tr) Prop | 1 step |
| 2 | 1. Tr: TermProp{i} 2. tr: Term TermProp{i} Type{i'} | Auto |
| 3 | 1. Tr: TermProp Term Type | Auto |
| 4 | TermProp{i} Type{i'} | Auto |
About:
 |  |  |  |  |