theorem grecaux2eq4 (z: nat) (K F: set) (_x1 _x2 n k: nat): $ _x1 = _x2 -> grecaux2 z K F _x1 n k = grecaux2 z K F _x2 n k $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | _x1 = _x2 -> _x1 = _x2 |
|
2 | 1 | grecaux2eq4d | _x1 = _x2 -> grecaux2 z K F _x1 n k = grecaux2 z K F _x2 n k |