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

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