apply IsDeduct.axiom_
case h1.h1.a.a.h1.h1.h1.h1
x y : VarName
⊢ IsDeduct ∅
    (forall_ y (forall_ x (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))))))
case h1.h1.a.a.h1.h1.h1.h1.a
x y : VarName
⊢ IsAxiom (forall_ y (forall_ x (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))))))