Theorem: FOL.NV.T_18_2
Proof state before:
U V P_U P_V : Formula
l : List VarName
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (P_U.iff_ P_V))
Tactic:
induction h1
Proof state after:
case same_
U V P_U P_V : Formula
l : List VarName
P_u✝ P_v✝ : Formula
a✝ : P_u✝ = P_v✝
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝ → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.iff_ P_v✝))

case diff_
U V P_U P_V : Formula
l : List VarName
P_u✝ P_v✝ : Formula
a✝¹ : P_u✝ = U
a✝ : P_v✝ = V
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝ → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.iff_ P_v✝))

case not_
U V P_U P_V : Formula
l : List VarName
P_u✝ P_v✝ : Formula
a✝ : IsReplOfFormulaInFormula U V P_u✝ P_v✝
a_ih✝ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.iff_ P_v✝))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝.not_ → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.not_.iff_ P_v✝.not_))

case imp_
U V P_U P_V : Formula
l : List VarName
P_u✝ Q_u✝ P_v✝ Q_v✝ : Formula
a✝¹ : IsReplOfFormulaInFormula U V P_u✝ P_v✝
a✝ : IsReplOfFormulaInFormula U V Q_u✝ Q_v✝
a_ih✝¹ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.iff_ P_v✝))
a_ih✝ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v Q_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (Q_u✝.iff_ Q_v✝))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v (P_u✝.imp_ Q_u✝) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((P_u✝.imp_ Q_u✝).iff_ (P_v✝.imp_ Q_v✝)))

case and_
U V P_U P_V : Formula
l : List VarName
P_u✝ Q_u✝ P_v✝ Q_v✝ : Formula
a✝¹ : IsReplOfFormulaInFormula U V P_u✝ P_v✝
a✝ : IsReplOfFormulaInFormula U V Q_u✝ Q_v✝
a_ih✝¹ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.iff_ P_v✝))
a_ih✝ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v Q_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (Q_u✝.iff_ Q_v✝))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v (P_u✝.and_ Q_u✝) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((P_u✝.and_ Q_u✝).iff_ (P_v✝.and_ Q_v✝)))

case or_
U V P_U P_V : Formula
l : List VarName
P_u✝ Q_u✝ P_v✝ Q_v✝ : Formula
a✝¹ : IsReplOfFormulaInFormula U V P_u✝ P_v✝
a✝ : IsReplOfFormulaInFormula U V Q_u✝ Q_v✝
a_ih✝¹ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.iff_ P_v✝))
a_ih✝ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v Q_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (Q_u✝.iff_ Q_v✝))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v (P_u✝.or_ Q_u✝) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((P_u✝.or_ Q_u✝).iff_ (P_v✝.or_ Q_v✝)))

case iff_
U V P_U P_V : Formula
l : List VarName
P_u✝ Q_u✝ P_v✝ Q_v✝ : Formula
a✝¹ : IsReplOfFormulaInFormula U V P_u✝ P_v✝
a✝ : IsReplOfFormulaInFormula U V Q_u✝ Q_v✝
a_ih✝¹ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.iff_ P_v✝))
a_ih✝ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v Q_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (Q_u✝.iff_ Q_v✝))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v (P_u✝.iff_ Q_u✝) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((P_u✝.iff_ Q_u✝).iff_ (P_v✝.iff_ Q_v✝)))

case forall_
U V P_U P_V : Formula
l : List VarName
x✝ : VarName
P_u✝ P_v✝ : Formula
a✝ : IsReplOfFormulaInFormula U V P_u✝ P_v✝
a_ih✝ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.iff_ P_v✝))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v (forall_ x✝ P_u✝) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((forall_ x✝ P_u✝).iff_ (forall_ x✝ P_v✝)))

case exists_
U V P_U P_V : Formula
l : List VarName
x✝ : VarName
P_u✝ P_v✝ : Formula
a✝ : IsReplOfFormulaInFormula U V P_u✝ P_v✝
a_ih✝ :
  (∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_u✝ → v ∈ l) →
    IsProof ((Forall_ l (U.iff_ V)).imp_ (P_u✝.iff_ P_v✝))
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v (exists_ x✝ P_u✝) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((exists_ x✝ P_u✝).iff_ (exists_ x✝ P_v✝)))