Nuprl - Proof: delete fenum value comp1 gen 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: delete fenum value comp1 gen 1 1 1

1. P :

Prop
2. Q :

Prop
3. f : {u:

| P(u) }

{v:

| Q(v) }
4. Inj({u:

| P(u) }; {u:

| Q(u) }; f)
5. m : {u:

| P(u) }
6. k : {v:

| Q(v) }
7. i : {u:

| P(u) &

u = m }
8. f(i) = k
9. f(m)

{v:

| Q(v) }

f(m)

{v:

| Q(v) &

v = k }

By:	Guarding (f(<arg>)) Analyze-1 THEN Guarding (f(<arg>)) Analyze

Generated subgoal:

1 9. f(m)
10. Q(f(m))
f(m) = k
2 steps

About:

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