Nuprl - Proof: rel exp wf

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel exp wf

, T:Type, R:(T

Prop). R^n

Prop

By:	InductionOnNat THEN RecUnfold `rel_exp` 0 THEN Reduce 0 THEN Try (Complete Auto) THEN SplitOnConclITE

Generated subgoal:

1 1. n :
2. 0<n
3. T:Type, R:(TTProp). R^n-1 TTProp
4. n = 0
5. T : Type
6. R : TTProp
7. T
8. y : T
9. z : T
(z R^n-1 y) Prop
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html