simp only [def_and_]
case h1.h1.h1.a.a
x y z : VarName
⊢ IsDeduct ∅
    ((((eq_ x y).and_ (eq_ z z)).imp_ (((eq_ x z).imp_ (eq_ y z)).and_ ((eq_ y z).imp_ (eq_ x z)))).imp_
      ((eq_ z z).imp_ (((eq_ x y).and_ (eq_ y z)).imp_ (eq_ x z))))
case h1.h1.h1.a.a
x y z : VarName
⊢ IsDeduct ∅
    ((((eq_ x y).imp_ (eq_ z z).not_).not_.imp_
          (((eq_ x z).imp_ (eq_ y z)).imp_ ((eq_ y z).imp_ (eq_ x z)).not_).not_).imp_
      ((eq_ z z).imp_ (((eq_ x y).imp_ (eq_ y z).not_).not_.imp_ (eq_ x z))))