exact IsAxiom.eq_2_eq_ x z y z
case h1.h1.h1.a.a.h1.h1.h1.h1.a
x y z : VarName
⊢ IsAxiom (forall_ x (forall_ z (forall_ y (forall_ z (((eq_ x y).and_ (eq_ z z)).imp_ ((eq_ x z).iff_ (eq_ y z)))))))
no goals