Nuprl - Proof: card nsub inj vs lopped 1 1 1 2

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

1. a :

2. b :

3. f :

a inj

(a-1) inj

{x:

x = f(a-1) }

By:	BackThru: Thm* a:, b:, f:(a inj b). f (a-1) inj {x:b\| x = f(a-1) }

Generated subgoals:

None

About:

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