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

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