Nuprl - Proof: listify length 1 1 1

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

1. T : Type
2. m :

3. n :

4. f : {m..n

}

T
5. m

||f{m..n

}|| = n-m

By:	Assert (m:{...n}, f:({m..n}T). \|\|f{m..n}\|\| = n-m) THENA OnHyps [5;4;2] Thin

Generated subgoals:

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

2 6. m:{...n}, f:({m..n}T). ||f{m..n}|| = n-m
||f{m..n}|| = n-m
1 step

About:

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

1	2. n : m:{...n}, f:({m..n}T). \|\|f{m..n}\|\| = n-m	4 steps
2	6. m:{...n}, f:({m..n}T). \|\|f{m..n}\|\| = n-m \|\|f{m..n}\|\| = n-m	1 step