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

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

1. P :

Prop
2. Q :

Prop
3. f : {u:

| P(u) }

{v:

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

| P(k) }; {k:

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

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

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

| P(u) &

u = m }
8. f(m)

9. Q(f(m))
10. f(i)

11. Q(f(i))
12. i

13. P(i)
14.

i = m

if f(i)=

f(m) else f(i) fi

{v:

| Q(v) &

v = k }

By:	SplitITE Concl

Generated subgoals:

1 15. f(i) = k
  f(m)  {v:| Q(v) & v = k }
3 steps

2 15. f(i)  k
  f(i)  {v:| Q(v) & v = k }
1 step

About:

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

1	15. f(i) = k f(m) {v:\| Q(v) & v = k }	3 steps
2	15. f(i) k f(i) {v:\| Q(v) & v = k }	1 step