simp only [def_and_]
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ¬(h1_x ∉ l ∧ isFreeIn h1_x ((U.imp_ V).and_ (V.imp_ U)))
case h1.a.h2
U V P_U P_V : Formula
l : List VarName
h1_x : VarName
h1_P h1_P' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_ih :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
h2 : ∀ (v : VarName), isFreeIn v U ∨ isFreeIn v V → v = h1_x ∨ isBoundIn v h1_P → v ∈ l
⊢ ¬(h1_x ∉ l ∧ isFreeIn h1_x ((U.imp_ V).imp_ (V.imp_ U).not_).not_)