Axiom E_equiv_e : forall x y : Z, E x y <-> e x y.