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

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