theorem grecaux2eq6 (z: nat) (K F: set) (x n _k1 _k2: nat): $ _k1 = _k2 -> grecaux2 z K F x n _k1 = grecaux2 z K F x n _k2 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | _k1 = _k2 -> _k1 = _k2 |
|
2 | 1 | grecaux2eq6d | _k1 = _k2 -> grecaux2 z K F x n _k1 = grecaux2 z K F x n _k2 |