Nuprl - Proof: delete fenum value is inj gen 1

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

1. P :

Prop
2. Q :

Prop
3. f : {u:

| P(u) }

{v:

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

| P(u) }; {v:

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

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

| Q(v) }
7. (Replace value k by f(m) in f)

{u:

| P(u) &

u = m }

{v:

| Q(v) &

v = k }
7. & Inj({u:

| P(u) &

u = m }; {v:

| Q(v) &

v = k };
7. & Inj(Replace value k by f(m) in f)

Inj({u:

| P(u) &

u = m }; {v:

| Q(v) &

v = k };

Inj(Replace value k by f(m) in f)

By:

Analyze-1

Generated subgoals:

None

About:

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