| Who Cites delete fenum value? |
|
delete_fenum_value | Def Replace value k by f(m) in f == Replace values x s.t. x= k by f(m) in f |
| | Thm* Inj({k: | P(k) }; {k: | Q(k) }; f)
Thm* 
Thm* ( m:{u: | P(u) }, k:{v: | Q(v) }.
Thm* ((Replace value k by f(m) in f)
Thm* ( {u: | P(u) & u = m } {v: | Q(v) & v = k }) |
| | Thm* Inj( (m+1); (k+1); f)  (Replace value k by f(m) in f) m  k |
|
eq_int | Def i= j == if i=j true ; false fi |
| | Thm* i,j: . (i= j)  |
|
replace_fn_values | Def (Replace values x s.t. P(x) by y in f)(i) == if P(f(i)) y else f(i) fi |
| | Thm* A,X:Type, P:(A  ), y:A, f:(X A).
Thm* (Replace values x s.t. P(x) by y in f) X A |