Nuprl - Proof: listify length 1

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

1. T : Type
2. m :

3. n :

4. f : {m..n

}

n<m

||f{m..n

}|| = n-m

By:	Decide (mn)

Generated subgoal:

1 5. mn
n<m ||f{m..n}|| = n-m
7 steps

About:

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