apply generalization
case h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y ((eq_ x y).imp_ (eq_ y x)))
case h1.h1
x y : VarName
⊢ IsDeduct ∅ ((eq_ x y).imp_ (eq_ y x))

case h1.h2
x y : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn y H