apply h2 v
case a.a
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (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'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q) → v ∈ l
v : VarName
a2 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q
⊢ v ∈ l
case a.a
U V P_U P_V : Formula
l : List VarName
h1_P h1_Q h1_P' h1_Q' : Formula
h1_1 : IsReplOfFormulaInFormula U V h1_P h1_P'
h1_2 : IsReplOfFormulaInFormula U V h1_Q h1_Q'
h1_ih_1 :
  (∀ (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'))
h1_ih_2 :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q) → v ∈ l
v : VarName
a2 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q
⊢ (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q)