Theorem: FOL.NV.T_18_2 (FOL/NV/Margaris/Fol.lean)

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
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✝)))

State before:
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : h1_P = h1_P'
h2 : ∀ (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'))
Tactic:
case same_ h1_P h1_P' h1_1 =>
  subst h1_1
  simp only [def_iff_]
  simp only [def_and_]
  SC
State after:
no goals

State before:
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : h1_P = U
h1_2 : h1_P' = V
h2 : ∀ (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'))
Tactic:
case diff_ h1_P h1_P' h1_1 h1_2 =>
  subst h1_1
  subst h1_2
  apply Forall_spec_id
State after:
no goals

State before:
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 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✝)))
Tactic:
all_goals
  sorry
State after:
no goals

State before:
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : h1_P = h1_P'
h2 : ∀ (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'))
Tactic:
subst h1_1
State after:
U V P_U P_V : Formula
l : List VarName
h1_P : Formula
h2 : ∀ (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))

State before:
U V P_U P_V : Formula
l : List VarName
h1_P : Formula
h2 : ∀ (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))
Tactic:
simp only [def_iff_]
State after:
U V P_U P_V : Formula
l : List VarName
h1_P : Formula
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.imp_ h1_P).and_ (h1_P.imp_ h1_P)))

State before:
U V P_U P_V : Formula
l : List VarName
h1_P : Formula
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.imp_ h1_P).and_ (h1_P.imp_ h1_P)))
Tactic:
simp only [def_and_]
State after:
U V P_U P_V : Formula
l : List VarName
h1_P : Formula
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_ ((h1_P.imp_ h1_P).imp_ (h1_P.imp_ h1_P).not_).not_)

State before:
U V P_U P_V : Formula
l : List VarName
h1_P : Formula
h2 : ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_ ((h1_P.imp_ h1_P).imp_ (h1_P.imp_ h1_P).not_).not_)
Tactic:
SC
State after:
no goals

State before:
U V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_1 : h1_P = U
h1_2 : h1_P' = V
h2 : ∀ (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'))
Tactic:
subst h1_1
State after:
V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_2 : h1_P' = V
h2 : ∀ (v : VarName), (isFreeIn v h1_P ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (h1_P.iff_ V)).imp_ (h1_P.iff_ h1_P'))

State before:
V P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h1_2 : h1_P' = V
h2 : ∀ (v : VarName), (isFreeIn v h1_P ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (h1_P.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Tactic:
subst h1_2
State after:
P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h2 : ∀ (v : VarName), (isFreeIn v h1_P ∨ isFreeIn v h1_P') ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (h1_P.iff_ h1_P')).imp_ (h1_P.iff_ h1_P'))

State before:
P_U P_V : Formula
l : List VarName
h1_P h1_P' : Formula
h2 : ∀ (v : VarName), (isFreeIn v h1_P ∨ isFreeIn v h1_P') ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (h1_P.iff_ h1_P')).imp_ (h1_P.iff_ h1_P'))
Tactic:
apply Forall_spec_id
State after:
no goals

State before:
U V P_U P_V : Formula
l : List 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) ∧ isBoundIn v h1_P.not_ → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.not_.iff_ h1_P'.not_))
Tactic:
simp only [isBoundIn] at h2
State after:
U V P_U P_V : Formula
l : List 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) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.not_.iff_ h1_P'.not_))

State before:
U V P_U P_V : Formula
l : List 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) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.not_.iff_ h1_P'.not_))
Tactic:
apply IsDeduct.mp_ ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
State after:
case a
U V P_U P_V : Formula
l : List 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) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P')).imp_ ((Forall_ l (U.iff_ V)).imp_ (h1_P.not_.iff_ h1_P'.not_)))

case a
U V P_U P_V : Formula
l : List 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) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅ ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))

State before:
case a
U V P_U P_V : Formula
l : List 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) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P')).imp_ ((Forall_ l (U.iff_ V)).imp_ (h1_P.not_.iff_ h1_P'.not_)))
Tactic:
simp only [def_iff_]
State after:
case a
U V P_U P_V : Formula
l : List 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) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.imp_ h1_P').and_ (h1_P'.imp_ h1_P))).imp_
      ((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.not_.imp_ h1_P'.not_).and_ (h1_P'.not_.imp_ h1_P.not_))))

State before:
case a
U V P_U P_V : Formula
l : List 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) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.imp_ h1_P').and_ (h1_P'.imp_ h1_P))).imp_
      ((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.not_.imp_ h1_P'.not_).and_ (h1_P'.not_.imp_ h1_P.not_))))
Tactic:
simp only [def_and_]
State after:
case a
U V P_U P_V : Formula
l : List 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) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_ ((h1_P.imp_ h1_P').imp_ (h1_P'.imp_ h1_P).not_).not_).imp_
      ((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_
        ((h1_P.not_.imp_ h1_P'.not_).imp_ (h1_P'.not_.imp_ h1_P.not_).not_).not_))

State before:
case a
U V P_U P_V : Formula
l : List 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) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_ ((h1_P.imp_ h1_P').imp_ (h1_P'.imp_ h1_P).not_).not_).imp_
      ((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_
        ((h1_P.not_.imp_ h1_P'.not_).imp_ (h1_P'.not_.imp_ h1_P.not_).not_).not_))
Tactic:
SC
State after:
no goals

State before:
case a
U V P_U P_V : Formula
l : List 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) ∧ isBoundIn v h1_P → v ∈ l
⊢ IsDeduct ∅ ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Tactic:
exact h1_ih h2
State after:
no goals

State before:
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.imp_ h1_Q) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((h1_P.imp_ h1_Q).iff_ (h1_P'.imp_ h1_Q')))
Tactic:
simp only [isBoundIn] at h2
State after:
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
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((h1_P.imp_ h1_Q).iff_ (h1_P'.imp_ h1_Q')))

State before:
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
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((h1_P.imp_ h1_Q).iff_ (h1_P'.imp_ h1_Q')))
Tactic:
apply IsDeduct.mp_ ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
State after:
case 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
⊢ IsDeduct ∅
    (((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P')).imp_
      ((Forall_ l (U.iff_ V)).imp_ ((h1_P.imp_ h1_Q).iff_ (h1_P'.imp_ h1_Q'))))

case 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
⊢ IsDeduct ∅ ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))

State before:
case 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
⊢ IsDeduct ∅
    (((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P')).imp_
      ((Forall_ l (U.iff_ V)).imp_ ((h1_P.imp_ h1_Q).iff_ (h1_P'.imp_ h1_Q'))))
Tactic:
apply IsDeduct.mp_ ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
State after:
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
⊢ IsDeduct ∅
    (((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q')).imp_
      (((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P')).imp_
        ((Forall_ l (U.iff_ V)).imp_ ((h1_P.imp_ h1_Q).iff_ (h1_P'.imp_ h1_Q')))))

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
⊢ IsDeduct ∅ ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))

State before:
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
⊢ IsDeduct ∅
    (((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q')).imp_
      (((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P')).imp_
        ((Forall_ l (U.iff_ V)).imp_ ((h1_P.imp_ h1_Q).iff_ (h1_P'.imp_ h1_Q')))))
Tactic:
simp only [def_iff_]
State after:
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
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_Q.imp_ h1_Q').and_ (h1_Q'.imp_ h1_Q))).imp_
      (((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.imp_ h1_P').and_ (h1_P'.imp_ h1_P))).imp_
        ((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_
          (((h1_P.imp_ h1_Q).imp_ (h1_P'.imp_ h1_Q')).and_ ((h1_P'.imp_ h1_Q').imp_ (h1_P.imp_ h1_Q))))))

State before:
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
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_Q.imp_ h1_Q').and_ (h1_Q'.imp_ h1_Q))).imp_
      (((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_ ((h1_P.imp_ h1_P').and_ (h1_P'.imp_ h1_P))).imp_
        ((Forall_ l ((U.imp_ V).and_ (V.imp_ U))).imp_
          (((h1_P.imp_ h1_Q).imp_ (h1_P'.imp_ h1_Q')).and_ ((h1_P'.imp_ h1_Q').imp_ (h1_P.imp_ h1_Q))))))
Tactic:
simp only [def_and_]
State after:
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
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_ ((h1_Q.imp_ h1_Q').imp_ (h1_Q'.imp_ h1_Q).not_).not_).imp_
      (((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_
            ((h1_P.imp_ h1_P').imp_ (h1_P'.imp_ h1_P).not_).not_).imp_
        ((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_
          (((h1_P.imp_ h1_Q).imp_ (h1_P'.imp_ h1_Q')).imp_ ((h1_P'.imp_ h1_Q').imp_ (h1_P.imp_ h1_Q)).not_).not_)))

State before:
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
⊢ IsDeduct ∅
    (((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_ ((h1_Q.imp_ h1_Q').imp_ (h1_Q'.imp_ h1_Q).not_).not_).imp_
      (((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_
            ((h1_P.imp_ h1_P').imp_ (h1_P'.imp_ h1_P).not_).not_).imp_
        ((Forall_ l ((U.imp_ V).imp_ (V.imp_ U).not_).not_).imp_
          (((h1_P.imp_ h1_Q).imp_ (h1_P'.imp_ h1_Q')).imp_ ((h1_P'.imp_ h1_Q').imp_ (h1_P.imp_ h1_Q)).not_).not_)))
Tactic:
SC
State after:
no goals

State before:
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
⊢ IsDeduct ∅ ((Forall_ l (U.iff_ V)).imp_ (h1_Q.iff_ h1_Q'))
Tactic:
apply h1_ih_2
State after:
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), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l

State before:
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), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_Q → v ∈ l
Tactic:
intro v a2
State after:
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

State before:
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
Tactic:
apply h2 v
State after:
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)

State before:
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)
Tactic:
tauto
State after:
no goals

State before:
case 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
⊢ IsDeduct ∅ ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Tactic:
apply h1_ih_1
State after:
case 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), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l

State before:
case 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), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
Tactic:
intro v a1
State after:
case 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
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P
⊢ v ∈ l

State before:
case 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
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P
⊢ v ∈ l
Tactic:
apply h2 v
State after:
case 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
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P
⊢ (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q)

State before:
case 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
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P
⊢ (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q)
Tactic:
cases a1
State after:
case a.intro
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
left✝ : isFreeIn v U ∨ isFreeIn v V
right✝ : isBoundIn v h1_P
⊢ (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q)

State before:
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
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ (isFreeIn v U ∨ isFreeIn v V) ∧ (isBoundIn v h1_P ∨ isBoundIn v h1_Q)
Tactic:
constructor
State after:
case left
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
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isFreeIn v U ∨ isFreeIn v V

case right
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
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isBoundIn v h1_P ∨ isBoundIn v h1_Q

State before:
case left
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
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isFreeIn v U ∨ isFreeIn v V
Tactic:
exact a1_left
State after:
no goals

State before:
case right
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
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isBoundIn v h1_P ∨ isBoundIn v h1_Q
Tactic:
left
State after:
case right.h
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
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isBoundIn v h1_P

State before:
case right.h
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
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isBoundIn v h1_P
Tactic:
exact a1_right
State after:
no goals

State before:
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) ∧ isBoundIn v (forall_ h1_x h1_P) → v ∈ l
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))
Tactic:
simp only [isBoundIn] at h2
State after:
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
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))

State before:
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
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))
Tactic:
simp at h2
State after:
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
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))

State before:
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
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))
Tactic:
apply deduction_theorem
State after:
case h1
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
⊢ IsDeduct (∅ ∪ {Forall_ l (U.iff_ V)}) ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P'))

State before:
case h1
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
⊢ IsDeduct (∅ ∪ {Forall_ l (U.iff_ V)}) ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P'))
Tactic:
simp
State after:
case h1
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
⊢ IsDeduct {Forall_ l (U.iff_ V)} ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P'))

State before:
case h1
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
⊢ IsDeduct {Forall_ l (U.iff_ V)} ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P'))
Tactic:
apply IsDeduct.mp_ (forall_ h1_x (h1_P.iff_ h1_P'))
State after:
case h1.a
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
⊢ IsDeduct {Forall_ l (U.iff_ V)}
    ((forall_ h1_x (h1_P.iff_ h1_P')).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))

case h1.a
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
⊢ IsDeduct {Forall_ l (U.iff_ V)} (forall_ h1_x (h1_P.iff_ h1_P'))

State before:
case h1.a
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
⊢ IsDeduct {Forall_ l (U.iff_ V)}
    ((forall_ h1_x (h1_P.iff_ h1_P')).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))
Tactic:
apply proof_imp_deduct
State after:
case h1.a.h1
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
⊢ IsProof ((forall_ h1_x (h1_P.iff_ h1_P')).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))

State before:
case h1.a.h1
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
⊢ IsProof ((forall_ h1_x (h1_P.iff_ h1_P')).imp_ ((forall_ h1_x h1_P).iff_ (forall_ h1_x h1_P')))
Tactic:
apply T_18_1
State after:
no goals

State before:
case h1.a
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
⊢ IsDeduct {Forall_ l (U.iff_ V)} (forall_ h1_x (h1_P.iff_ h1_P'))
Tactic:
apply generalization
State after:
case h1.a.h1
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
⊢ IsDeduct {Forall_ l (U.iff_ V)} (h1_P.iff_ h1_P')

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
⊢ ∀ H ∈ {Forall_ l (U.iff_ V)}, ¬isFreeIn h1_x H

State before:
case h1.a.h1
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
⊢ IsDeduct {Forall_ l (U.iff_ V)} (h1_P.iff_ h1_P')
Tactic:
apply IsDeduct.mp_ (Forall_ l (U.iff_ V))
State after:
case h1.a.h1.a
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
⊢ IsDeduct {Forall_ l (U.iff_ V)} ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))

case h1.a.h1.a
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
⊢ IsDeduct {Forall_ l (U.iff_ V)} (Forall_ l (U.iff_ V))

State before:
case h1.a.h1.a
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
⊢ IsDeduct {Forall_ l (U.iff_ V)} ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Tactic:
apply proof_imp_deduct
State after:
case h1.a.h1.a.h1
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
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))

State before:
case h1.a.h1.a.h1
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
⊢ IsProof ((Forall_ l (U.iff_ V)).imp_ (h1_P.iff_ h1_P'))
Tactic:
apply h1_ih
State after:
case h1.a.h1.a.h1
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
⊢ ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l

State before:
case h1.a.h1.a.h1
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
⊢ ∀ (v : VarName), (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P → v ∈ l
Tactic:
intro v a1
State after:
case h1.a.h1.a.h1
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
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P
⊢ v ∈ l

State before:
case h1.a.h1.a.h1
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
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v h1_P
⊢ v ∈ l
Tactic:
cases a1
State after:
case h1.a.h1.a.h1.intro
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
v : VarName
left✝ : isFreeIn v U ∨ isFreeIn v V
right✝ : isBoundIn v h1_P
⊢ v ∈ l

State before:
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
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ v ∈ l
Tactic:
case _ a1_left a1_right =>
  apply h2 v a1_left
  right
  apply a1_right
State after:
no goals

State before:
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
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ v ∈ l
Tactic:
apply h2 v a1_left
State after:
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
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ v = h1_x ∨ isBoundIn v h1_P

State before:
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
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ v = h1_x ∨ isBoundIn v h1_P
Tactic:
right
State after:
case h
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
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isBoundIn v h1_P

State before:
case h
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
v : VarName
a1_left : isFreeIn v U ∨ isFreeIn v V
a1_right : isBoundIn v h1_P
⊢ isBoundIn v h1_P
Tactic:
apply a1_right
State after:
no goals

State before:
case h1.a.h1.a
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
⊢ IsDeduct {Forall_ l (U.iff_ V)} (Forall_ l (U.iff_ V))
Tactic:
apply IsDeduct.assume_
State after:
case h1.a.h1.a.a
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
⊢ Forall_ l (U.iff_ V) ∈ {Forall_ l (U.iff_ V)}

State before:
case h1.a.h1.a.a
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
⊢ Forall_ l (U.iff_ V) ∈ {Forall_ l (U.iff_ V)}
Tactic:
simp
State after:
no goals

State before:
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
⊢ ∀ H ∈ {Forall_ l (U.iff_ V)}, ¬isFreeIn h1_x H
Tactic:
intro H a1
State after:
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
H : Formula
a1 : H ∈ {Forall_ l (U.iff_ V)}
⊢ ¬isFreeIn h1_x H

State before:
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
H : Formula
a1 : H ∈ {Forall_ l (U.iff_ V)}
⊢ ¬isFreeIn h1_x H
Tactic:
simp at a1
State after:
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
H : Formula
a1 : H = Forall_ l (U.iff_ V)
⊢ ¬isFreeIn h1_x H

State before:
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
H : Formula
a1 : H = Forall_ l (U.iff_ V)
⊢ ¬isFreeIn h1_x H
Tactic:
subst a1
State after:
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
⊢ ¬isFreeIn h1_x (Forall_ l (U.iff_ V))

State before:
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
⊢ ¬isFreeIn h1_x (Forall_ l (U.iff_ V))
Tactic:
simp only [Forall_isFreeIn]
State after:
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.iff_ V))

State before:
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.iff_ V))
Tactic:
simp only [def_iff_]
State after:
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)))

State before:
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)))
Tactic:
simp only [def_and_]
State after:
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_)

State before:
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_)
Tactic:
simp only [isFreeIn]
State after:
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 ∨ isFreeIn h1_x V) ∨ isFreeIn h1_x V ∨ isFreeIn h1_x U))

State before:
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 ∨ isFreeIn h1_x V) ∨ isFreeIn h1_x V ∨ isFreeIn h1_x U))
Tactic:
sorry
State after:
no goals

State before:
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✝)))
Tactic:
sorry
State after:
no goals