theorem grecaux2eq2 (z: nat) (_K1 _K2 F: set) (x n k: nat): $ _K1 == _K2 -> grecaux2 z _K1 F x n k = grecaux2 z _K2 F x n k $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | _K1 == _K2 -> _K1 == _K2 |
|
2 | 1 | grecaux2eq2d | _K1 == _K2 -> grecaux2 z _K1 F x n k = grecaux2 z _K2 F x n k |