Nuprl - Proof: listify length 1 1

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

1. T : Type
2. m :

3. n :

4. f : {m..n

}

T
5. m

n<m

||f{m..n

}|| = n-m

By:	Sel 2 (Analyze 0)

Generated subgoal:

1 ||f{m..n}|| = n-m
6 steps

About:

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