theorem grecaux2eq3 (z: nat) (K _F1 _F2: set) (x n k: nat): $ _F1 == _F2 -> grecaux2 z K _F1 x n k = grecaux2 z K _F2 x n k $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | _F1 == _F2 -> _F1 == _F2 |
|
2 | 1 | grecaux2eq3d | _F1 == _F2 -> grecaux2 z K _F1 x n k = grecaux2 z K _F2 x n k |