Nuprl - Proof: listify length 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: listify length 1 1 1 1

1. T : Type
2. n :

m:{...n}, f:({m..n

}

T). ||f{m..n

}|| = n-m

By:	(BackThru (Thm* i:, E:({...i}Prop). (Thm* E(i) (k:{...i-1}. E(k+1) E(k)) (k:{...i}. E(k))) THEN UnivCD

Generated subgoals:

1 3. f : {n..n}T
||f{n..n}|| = n-n
1 step

2 3. m : {...n-1}
4. f:({(m+1)..n}T). ||f{(m+1)..n}|| = n-(m+1)
5. f : {m..n}T
||f{m..n}|| = n-m
2 steps

About:

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

1	3. f : {n..n}T \|\|f{n..n}\|\| = n-n	1 step
2	3. m : {...n-1} 4. f:({(m+1)..n}T). \|\|f{(m+1)..n}\|\| = n-(m+1) 5. f : {m..n}T \|\|f{m..n}\|\| = n-m	2 steps