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

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