Nuprl - Proof: card nsub inj vs lopped 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card nsub inj vs lopped 1

1. a :

2. b :

(

a inj

b) ~ (

(

(a-1) inj

(b-1)))

By:	OOCinterpolate (i:b(a-1) inj {x:b\| x = i })

Generated subgoals:

1 (a inj b) ~ (i:b(a-1) inj {x:b| x = i })
28 steps

2 (i:b(a-1) inj {x:b| x = i }) ~ (b((a-1) inj (b-1)))
1 step

About:

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

1	(a inj b) ~ (i:b(a-1) inj {x:b\| x = i })	28 steps
2	(i:b(a-1) inj {x:b\| x = i }) ~ (b((a-1) inj (b-1)))	1 step