theorem grecaux2eq1 (_z1 _z2: nat) (K F: set) (x n k: nat): $ _z1 = _z2 -> grecaux2 _z1 K F x n k = grecaux2 _z2 K F x n k $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | _z1 = _z2 -> _z1 = _z2 |
|
| 2 | 1 | grecaux2eq1d | _z1 = _z2 -> grecaux2 _z1 K F x n k = grecaux2 _z2 K F x n k |