Nuprl - Proof: comp nat ind tp 1 1 1 1 1 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: comp nat ind tp 1 1 1 1 1 1 2 1

1. P :

Prop
2.

. (

. j<i

P(j))

P(i)
3. zz :

4. 0<zz
5.

. i<zz-1

P(i)
6. i :

7. i<zz

P(i)

By:	p. let i var_of_hyp -2 p , let j get_distinct_var i p , let Pi concl p , let Pj subst [i,(mvt j)] Pi in Assert (mk_all_term j (mk_implies_term (mk_less_than_term (mvt j) (mvt i)) Pj)) p

Generated subgoals:

1   i1:. i1<i  P(i1)
6 steps

2 8. i1:. i1<i  P(i1)
  P(i)
2 steps

About:

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