theorem grecaux2eq5 (z: nat) (K F: set) (x _n1 _n2 k: nat): $ _n1 = _n2 -> grecaux2 z K F x _n1 k = grecaux2 z K F x _n2 k $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | _n1 = _n2 -> _n1 = _n2 |
|
2 | 1 | grecaux2eq5d | _n1 = _n2 -> grecaux2 z K F x _n1 k = grecaux2 z K F x _n2 k |