Theorem grecaux1eq3 ≪ | index | src | ≫

theorem grecaux1eq3 (K: set) (x _z1 _z2 n: nat):
  $ _z1 = _z2 -> grecaux1 K x _z1 n = grecaux1 K x _z2 n $;

_z1 = _z2 -> _z1 = _z2

_z1 = _z2 -> grecaux1 K x _z1 n = grecaux1 K x _z2 n

Axiom use