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
(Replace value k by f(m) in f)(i) = f(i) 
{v:| Q(v) & v = k }Prop
Prop
| P(u) }{v:| Q(v) }
| P(u) }; {u:| Q(u) }; f)
| P(u) }
| Q(v) }
| P(u) & u = m }
f(i) = k
(Replace value k by f(m) in f)(i) = f(i) {v:| Q(v) & v = k }| By: |
 if f(i)= k f(m) else f(i) fi
THEN SplitITE Concl |
| 1 |
 k
f(i) = f(i) {v:| Q(v) & v = k } | 1 step |
About:
 |  |  |  |
 |  |  |  |  |  |