Theorem: FOL.NV.Program.Backend.soundness (FOL/NV/Program/Backend.lean)

State before:
Δ : List Formula
F : Formula
h1 : IsDeduct Δ F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ, Holds D I V E H) → Holds D I V E F
Tactic:
induction h1
State after:
case struct_1_
Δ : List Formula
F : Formula
Δ✝ : List Formula
H✝ phi✝ : Formula
a✝ : IsDeduct Δ✝ phi✝
a_ih✝ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ✝, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ H✝ :: Δ✝, Holds D I V E H) → Holds D I V E phi✝

case struct_2_
Δ : List Formula
F : Formula
Δ✝ : List Formula
H✝ phi✝ : Formula
a✝ : IsDeduct (H✝ :: H✝ :: Δ✝) phi✝
a_ih✝ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ H✝ :: H✝ :: Δ✝, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ H✝ :: Δ✝, Holds D I V E H) → Holds D I V E phi✝

case struct_3_
Δ : List Formula
F : Formula
Δ_1✝ Δ_2✝ : List Formula
H_1✝ H_2✝ phi✝ : Formula
a✝ : IsDeduct (Δ_1✝ ++ [H_1✝] ++ [H_2✝] ++ Δ_2✝) phi✝
a_ih✝ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1✝ ++ [H_1✝] ++ [H_2✝] ++ Δ_2✝, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1✝ ++ [H_2✝] ++ [H_1✝] ++ Δ_2✝, Holds D I V E H) → Holds D I V E phi✝

case assume_
Δ : List Formula
F phi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [phi✝], Holds D I V E H) → Holds D I V E phi✝

case prop_0_
Δ : List Formula
F : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E true_

case prop_1_
Δ : List Formula
F phi✝ psi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (phi✝.imp_ (psi✝.imp_ phi✝))

case prop_2_
Δ : List Formula
F phi✝ psi✝ chi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E ((phi✝.imp_ (psi✝.imp_ chi✝)).imp_ ((phi✝.imp_ psi✝).imp_ (phi✝.imp_ chi✝)))

case prop_3_
Δ : List Formula
F phi✝ psi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi✝.not_.imp_ psi✝.not_).imp_ (psi✝.imp_ phi✝))

case mp_
Δ : List Formula
F : Formula
Δ✝ : List Formula
phi✝ psi✝ : Formula
a✝¹ : IsDeduct Δ✝ (phi✝.imp_ psi✝)
a✝ : IsDeduct Δ✝ phi✝
a_ih✝¹ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ✝, Holds D I V E H) → Holds D I V E (phi✝.imp_ psi✝)
a_ih✝ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ✝, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ✝, Holds D I V E H) → Holds D I V E psi✝

case dt_
Δ : List Formula
F : Formula
Δ✝ : List Formula
H✝ phi✝ : Formula
a✝ : IsDeduct (H✝ :: Δ✝) phi✝
a_ih✝ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ H✝ :: Δ✝, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ✝, Holds D I V E H) → Holds D I V E (H✝.imp_ phi✝)

case pred_1_
Δ : List Formula
F : Formula
v✝ : VarName
phi✝ psi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E ((forall_ v✝ (phi✝.imp_ psi✝)).imp_ ((forall_ v✝ phi✝).imp_ (forall_ v✝ psi✝)))

case pred_2_
Δ : List Formula
F : Formula
v✝ t✝ : VarName
phi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E ((forall_ v✝ phi✝).imp_ (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v✝ t✝) freshChar phi✝))

case pred_3_
Δ : List Formula
F : Formula
v✝ : VarName
phi✝ : Formula
a✝ : ¬isFreeIn v✝ phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (phi✝.imp_ (forall_ v✝ phi✝))

case gen_
Δ : List Formula
F : Formula
v✝ : VarName
phi✝ : Formula
a✝ : IsDeduct [] phi✝
a_ih✝ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (forall_ v✝ phi✝)

case eq_1_
Δ : List Formula
F : Formula
v✝ : VarName
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (eq_ v✝ v✝)

case eq_2_pred_var_
Δ : List Formula
F : Formula
name✝ : PredName
xs✝ ys✝ : List VarName
a✝ : xs✝.length = ys✝.length
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E
        ((List.foldr and_ true_ (List.zipWith eq_ xs✝ ys✝)).imp_ ((pred_var_ name✝ xs✝).iff_ (pred_var_ name✝ ys✝)))

case eq_2_eq_
Δ : List Formula
F : Formula
x_0✝ x_1✝ y_0✝ y_1✝ : VarName
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E (((eq_ x_0✝ y_0✝).and_ (eq_ x_1✝ y_1✝)).imp_ ((eq_ x_0✝ x_1✝).iff_ (eq_ y_0✝ y_1✝)))

case def_false_
Δ : List Formula
F : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (false_.iff_ true_.not_)

case def_and_
Δ : List Formula
F phi✝ psi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi✝.and_ psi✝).iff_ (phi✝.imp_ psi✝.not_).not_)

case def_or_
Δ : List Formula
F phi✝ psi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi✝.or_ psi✝).iff_ (phi✝.not_.imp_ psi✝))

case def_iff_
Δ : List Formula
F phi✝ psi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E
        (((phi✝.iff_ psi✝).imp_ ((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_).imp_
            (((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_.imp_ (phi✝.iff_ psi✝)).not_).not_

case def_exists_
Δ : List Formula
F : Formula
v✝ : VarName
phi✝ : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((exists_ v✝ phi✝).iff_ (forall_ v✝ phi✝.not_).not_)

case sub_
Δ : List Formula
F : Formula
Δ✝ : List Formula
phi✝ : Formula
τ✝ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ✝ phi✝
a_ih✝ :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ✝, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ List.map (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ✝) Δ✝, Holds D I V E H) →
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ✝ phi✝)

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
Tactic:
case struct_1_ Δ' H _ _ ih_2 =>
  intro D I V E a1
  apply ih_2
  intro H' a2
  simp at a1
  cases a1
  case _ a1_left a1_right =>
    exact a1_right H' a2
State after:
no goals

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
Tactic:
case struct_2_ Δ' H _ _ ih_2 =>
  intro D I V E a1
  apply ih_2
  intro H' a2
  simp at a1
  cases a1
  case _ a1_left a1_right =>
    simp at a2
    cases a2
    case _ a2 =>
      simp only [a2]
      exact a1_left
    case _ a2 =>
      exact a1_right H' a2
State after:
no goals

State before:
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
Tactic:
case struct_3_ Δ_1 Δ_2 H_1 H_2 _ _ ih_2 =>
  intro D I V E a1
  apply ih_2
  intro H' a2
  simp at a1
  apply a1
  simp at a2
  tauto
State after:
no goals

State before:
Δ : List Formula
F phi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [phi], Holds D I V E H) → Holds D I V E phi
Tactic:
case assume_ phi =>
  intro D I V E a1
  simp at a1
  exact a1
State after:
no goals

State before:
Δ : List Formula
F : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E true_
Tactic:
case prop_0_ =>
  intro D I V E _
  simp only [Holds]
State after:
no goals

State before:
Δ : List Formula
F phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (phi.imp_ (psi.imp_ phi))
Tactic:
case prop_1_ phi psi =>
  intro D I V E _
  simp only [Holds]
  tauto
State after:
no goals

State before:
Δ : List Formula
F phi psi chi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi.imp_ (psi.imp_ chi)).imp_ ((phi.imp_ psi).imp_ (phi.imp_ chi)))
Tactic:
case prop_2_ phi psi chi =>
  intro D I V E _
  simp only [Holds]
  tauto
State after:
no goals

State before:
Δ : List Formula
F phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi.not_.imp_ psi.not_).imp_ (psi.imp_ phi))
Tactic:
case prop_3_ phi psi =>
  intro D I V E _
  simp only [Holds]
  tauto
State after:
no goals

State before:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((forall_ v (phi.imp_ psi)).imp_ ((forall_ v phi).imp_ (forall_ v psi)))
Tactic:
case pred_1_ v phi psi =>
  intro D I V E _
  simp only [Holds]
  intro a2 a3 d
  apply a2 d
  exact a3 d
State after:
no goals

State before:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E ((forall_ v phi).imp_ (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi))
Tactic:
case pred_2_ v t phi =>
  intro D I V E _
  obtain s1 := FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem D I V E (Function.updateITE id v t) freshChar phi
  simp only [Holds]
  intro a2
  simp only [s1]
  simp only [Function.updateITE_comp_left]
  simp
  exact a2 (V t)
State after:
no goals

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (phi.imp_ (forall_ v phi))
Tactic:
case pred_3_ v phi ih =>
  intro D I V E _
  simp only [Holds]
  intro a2 d
  have s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
  {
    apply Holds_coincide_Var
    intro v' a1
    simp only [Function.updateITE]
    split_ifs
    case _ c1 =>
      subst c1
      contradiction
    case _ c1 =>
      rfl
  }
  simp only [s1]
  exact a2
State after:
no goals

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
a✝ : IsDeduct [] phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E phi
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (forall_ v phi)
Tactic:
case gen_ v phi _ ih_2 =>
  intro D I V E _
  simp only [Holds]
  intro d
  apply ih_2
  simp
State after:
no goals

State before:
Δ : List Formula
F : Formula
v : VarName
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (eq_ v v)
Tactic:
case eq_1_ v =>
  intro D I V E _
  simp only [Holds]
State after:
no goals

State before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E (((eq_ x_0 y_0).and_ (eq_ x_1 y_1)).imp_ ((eq_ x_0 x_1).iff_ (eq_ y_0 y_1)))
Tactic:
case eq_2_eq_ x_0 x_1 y_0 y_1 =>
  intro D I V E _
  simp only [Holds]
  intro a2
  cases a2
  case _ a2_left a2_right =>
    simp only [a2_left]
    simp only [a2_right]
State after:
no goals

State before:
Δ : List Formula
F : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (false_.iff_ true_.not_)
Tactic:
case def_false_ =>
  intro D I V E _
  simp only [Holds]
  tauto
State after:
no goals

State before:
Δ : List Formula
F phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi.and_ psi).iff_ (phi.imp_ psi.not_).not_)
Tactic:
case def_and_ phi psi =>
  intro D I V E _
  simp only [Holds]
  tauto
State after:
no goals

State before:
Δ : List Formula
F phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi.or_ psi).iff_ (phi.not_.imp_ psi))
Tactic:
case def_or_ phi psi =>
  intro D I V E _
  simp only [Holds]
  tauto
State after:
no goals

State before:
Δ : List Formula
F phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E
        (((phi.iff_ psi).imp_ ((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_).imp_
            (((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_.imp_ (phi.iff_ psi)).not_).not_
Tactic:
case def_iff_ phi psi =>
  intro D I V E _
  simp only [Holds]
  tauto
State after:
no goals

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((exists_ v phi).iff_ (forall_ v phi.not_).not_)
Tactic:
case def_exists_ v phi =>
  intro D I V E _
  simp only [Holds]
  simp
State after:
no goals

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ List.map (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ) Δ', Holds D I V E H) →
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Tactic:
case sub_ Δ' phi τ _ ih_2 =>
  intro D I V E a1
  simp at a1
  obtain s1 := Sub.Pred.All.Rec.Option.Fresh.substitution_theorem D I V E freshChar τ
  simp only [← s1] at a1
  simp only [← s1]
  apply ih_2
  exact a1
State after:
no goals

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
Tactic:
intro D I V E a1
State after:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
⊢ Holds D I V E phi✝

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
⊢ Holds D I V E phi✝
Tactic:
apply ih_2
State after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
⊢ ∀ H ∈ Δ', Holds D I V E H

State before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
⊢ ∀ H ∈ Δ', Holds D I V E H
Tactic:
intro H' a2
State after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
H' : Formula
a2 : H' ∈ Δ'
⊢ Holds D I V E H'

State before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
H' : Formula
a2 : H' ∈ Δ'
⊢ Holds D I V E H'
Tactic:
simp at a1
State after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ Δ'
a1 : Holds D I V E H ∧ ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'

State before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ Δ'
a1 : Holds D I V E H ∧ ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Tactic:
cases a1
State after:
case a.intro
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ Δ'
left✝ : Holds D I V E H
right✝ : ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ Δ'
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Tactic:
case _ a1_left a1_right =>
  exact a1_right H' a2
State after:
no goals

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct Δ' phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ Δ'
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Tactic:
exact a1_right H' a2
State after:
no goals

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
Tactic:
intro D I V E a1
State after:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
⊢ Holds D I V E phi✝

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
⊢ Holds D I V E phi✝
Tactic:
apply ih_2
State after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
⊢ ∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1

State before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
⊢ ∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1
Tactic:
intro H' a2
State after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
H' : Formula
a2 : H' ∈ H :: H :: Δ'
⊢ Holds D I V E H'

State before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
H' : Formula
a2 : H' ∈ H :: H :: Δ'
⊢ Holds D I V E H'
Tactic:
simp at a1
State after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ H :: H :: Δ'
a1 : Holds D I V E H ∧ ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'

State before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ H :: H :: Δ'
a1 : Holds D I V E H ∧ ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Tactic:
cases a1
State after:
case a.intro
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ H :: H :: Δ'
left✝ : Holds D I V E H
right✝ : ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ H :: H :: Δ'
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Tactic:
case _ a1_left a1_right =>
  simp at a2
  cases a2
  case _ a2 =>
    simp only [a2]
    exact a1_left
  case _ a2 =>
    exact a1_right H' a2
State after:
no goals

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ H :: H :: Δ'
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
⊢ Holds D I V E H'
Tactic:
simp at a2
State after:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' = H ∨ H' ∈ Δ'
⊢ Holds D I V E H'

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' = H ∨ H' ∈ Δ'
⊢ Holds D I V E H'
Tactic:
cases a2
State after:
case inl
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
h✝ : H' = H
⊢ Holds D I V E H'

case inr
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
h✝ : H' ∈ Δ'
⊢ Holds D I V E H'

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' = H
⊢ Holds D I V E H'
Tactic:
case _ a2 =>
  simp only [a2]
  exact a1_left
State after:
no goals

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' ∈ Δ'
⊢ Holds D I V E H'
Tactic:
case _ a2 =>
  exact a1_right H' a2
State after:
no goals

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' = H
⊢ Holds D I V E H'
Tactic:
simp only [a2]
State after:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' = H
⊢ Holds D I V E H

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' = H
⊢ Holds D I V E H
Tactic:
exact a1_left
State after:
no goals

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi✝ : Formula
a✝ : IsDeduct (H :: H :: Δ') phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: H :: Δ', Holds D I V E H_1) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a1_left : Holds D I V E H
a1_right : ∀ a ∈ Δ', Holds D I V E a
a2 : H' ∈ Δ'
⊢ Holds D I V E H'
Tactic:
exact a1_right H' a2
State after:
no goals

State before:
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
Tactic:
intro D I V E a1
State after:
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, Holds D I V E H
⊢ Holds D I V E phi✝

State before:
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, Holds D I V E H
⊢ Holds D I V E phi✝
Tactic:
apply ih_2
State after:
case a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, Holds D I V E H
⊢ ∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H

State before:
case a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, Holds D I V E H
⊢ ∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H
Tactic:
intro H' a2
State after:
case a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, Holds D I V E H
H' : Formula
a2 : H' ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2
⊢ Holds D I V E H'

State before:
case a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ_1 ++ [H_2] ++ [H_1] ++ Δ_2, Holds D I V E H
H' : Formula
a2 : H' ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2
⊢ Holds D I V E H'
Tactic:
simp at a1
State after:
case a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2
a1 : ∀ (H : Formula), H ∈ Δ_1 ∨ H = H_2 ∨ H = H_1 ∨ H ∈ Δ_2 → Holds D I V E H
⊢ Holds D I V E H'

State before:
case a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2
a1 : ∀ (H : Formula), H ∈ Δ_1 ∨ H = H_2 ∨ H = H_1 ∨ H ∈ Δ_2 → Holds D I V E H
⊢ Holds D I V E H'
Tactic:
apply a1
State after:
case a.a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2
a1 : ∀ (H : Formula), H ∈ Δ_1 ∨ H = H_2 ∨ H = H_1 ∨ H ∈ Δ_2 → Holds D I V E H
⊢ H' ∈ Δ_1 ∨ H' = H_2 ∨ H' = H_1 ∨ H' ∈ Δ_2

State before:
case a.a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a2 : H' ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2
a1 : ∀ (H : Formula), H ∈ Δ_1 ∨ H = H_2 ∨ H = H_1 ∨ H ∈ Δ_2 → Holds D I V E H
⊢ H' ∈ Δ_1 ∨ H' = H_2 ∨ H' = H_1 ∨ H' ∈ Δ_2
Tactic:
simp at a2
State after:
case a.a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a1 : ∀ (H : Formula), H ∈ Δ_1 ∨ H = H_2 ∨ H = H_1 ∨ H ∈ Δ_2 → Holds D I V E H
a2 : H' ∈ Δ_1 ∨ H' = H_1 ∨ H' = H_2 ∨ H' ∈ Δ_2
⊢ H' ∈ Δ_1 ∨ H' = H_2 ∨ H' = H_1 ∨ H' ∈ Δ_2

State before:
case a.a
Δ : List Formula
F : Formula
Δ_1 Δ_2 : List Formula
H_1 H_2 phi✝ : Formula
a✝ : IsDeduct (Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2) phi✝
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ_1 ++ [H_1] ++ [H_2] ++ Δ_2, Holds D I V E H) → Holds D I V E phi✝
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
H' : Formula
a1 : ∀ (H : Formula), H ∈ Δ_1 ∨ H = H_2 ∨ H = H_1 ∨ H ∈ Δ_2 → Holds D I V E H
a2 : H' ∈ Δ_1 ∨ H' = H_1 ∨ H' = H_2 ∨ H' ∈ Δ_2
⊢ H' ∈ Δ_1 ∨ H' = H_2 ∨ H' = H_1 ∨ H' ∈ Δ_2
Tactic:
tauto
State after:
no goals

State before:
Δ : List Formula
F phi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [phi], Holds D I V E H) → Holds D I V E phi
Tactic:
intro D I V E a1
State after:
Δ : List Formula
F phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ [phi], Holds D I V E H
⊢ Holds D I V E phi

State before:
Δ : List Formula
F phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ [phi], Holds D I V E H
⊢ Holds D I V E phi
Tactic:
simp at a1
State after:
Δ : List Formula
F phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : Holds D I V E phi
⊢ Holds D I V E phi

State before:
Δ : List Formula
F phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : Holds D I V E phi
⊢ Holds D I V E phi
Tactic:
exact a1
State after:
no goals

State before:
Δ : List Formula
F : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E true_
Tactic:
intro D I V E _
State after:
Δ : List Formula
F : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E true_

State before:
Δ : List Formula
F : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E true_
Tactic:
simp only [Holds]
State after:
no goals

State before:
Δ : List Formula
F phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (phi.imp_ (psi.imp_ phi))
Tactic:
intro D I V E _
State after:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (phi.imp_ (psi.imp_ phi))

State before:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (phi.imp_ (psi.imp_ phi))
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E phi → Holds D I V E psi → Holds D I V E phi

State before:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E phi → Holds D I V E psi → Holds D I V E phi
Tactic:
tauto
State after:
no goals

State before:
Δ : List Formula
F phi psi chi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi.imp_ (psi.imp_ chi)).imp_ ((phi.imp_ psi).imp_ (phi.imp_ chi)))
Tactic:
intro D I V E _
State after:
Δ : List Formula
F phi psi chi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((phi.imp_ (psi.imp_ chi)).imp_ ((phi.imp_ psi).imp_ (phi.imp_ chi)))

State before:
Δ : List Formula
F phi psi chi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((phi.imp_ (psi.imp_ chi)).imp_ ((phi.imp_ psi).imp_ (phi.imp_ chi)))
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F phi psi chi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (Holds D I V E phi → Holds D I V E psi → Holds D I V E chi) →
    (Holds D I V E phi → Holds D I V E psi) → Holds D I V E phi → Holds D I V E chi

State before:
Δ : List Formula
F phi psi chi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (Holds D I V E phi → Holds D I V E psi → Holds D I V E chi) →
    (Holds D I V E phi → Holds D I V E psi) → Holds D I V E phi → Holds D I V E chi
Tactic:
tauto
State after:
no goals

State before:
Δ : List Formula
F phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi.not_.imp_ psi.not_).imp_ (psi.imp_ phi))
Tactic:
intro D I V E _
State after:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((phi.not_.imp_ psi.not_).imp_ (psi.imp_ phi))

State before:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((phi.not_.imp_ psi.not_).imp_ (psi.imp_ phi))
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (¬Holds D I V E phi → ¬Holds D I V E psi) → Holds D I V E psi → Holds D I V E phi

State before:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (¬Holds D I V E phi → ¬Holds D I V E psi) → Holds D I V E psi → Holds D I V E phi
Tactic:
tauto
State after:
no goals

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E (phi.imp_ psi)
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E psi
Tactic:
intro D I V E a1
State after:
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E (phi.imp_ psi)
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
⊢ Holds D I V E psi

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E (phi.imp_ psi)
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
⊢ Holds D I V E psi
Tactic:
simp only [Holds] at ih_major
State after:
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ Holds D I V E psi

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ Holds D I V E psi
Tactic:
apply ih_major
State after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ ∀ H ∈ Δ', Holds D I V E H

case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ Holds D I V E phi

State before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ ∀ H ∈ Δ', Holds D I V E H
Tactic:
intro H' a2
State after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
H' : Formula
a2 : H' ∈ Δ'
⊢ Holds D I V E H'

State before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
H' : Formula
a2 : H' ∈ Δ'
⊢ Holds D I V E H'
Tactic:
exact a1 H' a2
State after:
no goals

State before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ Holds D I V E phi
Tactic:
apply ih_minor
State after:
case a.a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ ∀ H ∈ Δ', Holds D I V E H

State before:
case a.a
Δ : List Formula
F : Formula
Δ' : List Formula
phi psi : Formula
a✝¹ : IsDeduct Δ' (phi.imp_ psi)
a✝ : IsDeduct Δ' phi
ih_minor :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
ih_major :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi → Holds D I V E psi
⊢ ∀ H ∈ Δ', Holds D I V E H
Tactic:
exact a1
State after:
no goals

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E (H.imp_ phi)
Tactic:
intro D I V E a1
State after:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
⊢ Holds D I V E (H.imp_ phi)

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
⊢ Holds D I V E (H.imp_ phi)
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
⊢ Holds D I V E H → Holds D I V E phi

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
⊢ Holds D I V E H → Holds D I V E phi
Tactic:
intro a2
State after:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ Holds D I V E phi

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ Holds D I V E phi
Tactic:
apply ih_2
State after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ ∀ H_1 ∈ H :: Δ', Holds D I V E H_1

State before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ ∀ H_1 ∈ H :: Δ', Holds D I V E H_1
Tactic:
simp
State after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ Holds D I V E H ∧ ∀ a ∈ Δ', Holds D I V E a

State before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ Holds D I V E H ∧ ∀ a ∈ Δ', Holds D I V E a
Tactic:
constructor
State after:
case a.left
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ Holds D I V E H

case a.right
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ ∀ a ∈ Δ', Holds D I V E a

State before:
case a.left
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ Holds D I V E H
Tactic:
exact a2
State after:
no goals

State before:
case a.right
Δ : List Formula
F : Formula
Δ' : List Formula
H phi : Formula
a✝ : IsDeduct (H :: Δ') phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H_1 ∈ H :: Δ', Holds D I V E H_1) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ Δ', Holds D I V E H
a2 : Holds D I V E H
⊢ ∀ a ∈ Δ', Holds D I V E a
Tactic:
exact a1
State after:
no goals

State before:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((forall_ v (phi.imp_ psi)).imp_ ((forall_ v phi).imp_ (forall_ v psi)))
Tactic:
intro D I V E _
State after:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((forall_ v (phi.imp_ psi)).imp_ ((forall_ v phi).imp_ (forall_ v psi)))

State before:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((forall_ v (phi.imp_ psi)).imp_ ((forall_ v phi).imp_ (forall_ v psi)))
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (∀ (d : D), Holds D I (Function.updateITE V v d) E phi → Holds D I (Function.updateITE V v d) E psi) →
    (∀ (d : D), Holds D I (Function.updateITE V v d) E phi) → ∀ (d : D), Holds D I (Function.updateITE V v d) E psi

State before:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (∀ (d : D), Holds D I (Function.updateITE V v d) E phi → Holds D I (Function.updateITE V v d) E psi) →
    (∀ (d : D), Holds D I (Function.updateITE V v d) E phi) → ∀ (d : D), Holds D I (Function.updateITE V v d) E psi
Tactic:
intro a2 a3 d
State after:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi → Holds D I (Function.updateITE V v d) E psi
a3 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E psi

State before:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi → Holds D I (Function.updateITE V v d) E psi
a3 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E psi
Tactic:
apply a2 d
State after:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi → Holds D I (Function.updateITE V v d) E psi
a3 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E phi

State before:
Δ : List Formula
F : Formula
v : VarName
phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi → Holds D I (Function.updateITE V v d) E psi
a3 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E phi
Tactic:
exact a3 d
State after:
no goals

State before:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E ((forall_ v phi).imp_ (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi))
Tactic:
intro D I V E _
State after:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((forall_ v phi).imp_ (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi))

State before:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((forall_ v phi).imp_ (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi))
Tactic:
obtain s1 := FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem D I V E (Function.updateITE id v t) freshChar phi
State after:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
⊢ Holds D I V E ((forall_ v phi).imp_ (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi))

State before:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
⊢ Holds D I V E ((forall_ v phi).imp_ (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi))
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
⊢ (∀ (d : D), Holds D I (Function.updateITE V v d) E phi) →
    Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi)

State before:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
⊢ (∀ (d : D), Holds D I (Function.updateITE V v d) E phi) →
    Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi)
Tactic:
intro a2
State after:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
⊢ Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi)

State before:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
⊢ Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi)
Tactic:
simp only [s1]
State after:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
⊢ Holds D I (V ∘ Function.updateITE id v t) E phi

State before:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
⊢ Holds D I (V ∘ Function.updateITE id v t) E phi
Tactic:
simp only [Function.updateITE_comp_left]
State after:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
⊢ Holds D I (Function.updateITE (V ∘ id) v (V t)) E phi

State before:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
⊢ Holds D I (Function.updateITE (V ∘ id) v (V t)) E phi
Tactic:
simp
State after:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
⊢ Holds D I (Function.updateITE V v (V t)) E phi

State before:
Δ : List Formula
F : Formula
v t : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
s1 :
  Holds D I V E (Sub.Var.All.Rec.Fresh.sub (Function.updateITE id v t) freshChar phi) ↔
    Holds D I (V ∘ Function.updateITE id v t) E phi
a2 : ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
⊢ Holds D I (Function.updateITE V v (V t)) E phi
Tactic:
exact a2 (V t)
State after:
no goals

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (phi.imp_ (forall_ v phi))
Tactic:
intro D I V E _
State after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (phi.imp_ (forall_ v phi))

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (phi.imp_ (forall_ v phi))
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E phi → ∀ (d : D), Holds D I (Function.updateITE V v d) E phi

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E phi → ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
Tactic:
intro a2 d
State after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E phi

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E phi
Tactic:
have s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
State after:
case s1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi

Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
⊢ Holds D I (Function.updateITE V v d) E phi

State before:
case s1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi

Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
⊢ Holds D I (Function.updateITE V v d) E phi
Tactic:
{
  apply Holds_coincide_Var
  intro v' a1
  simp only [Function.updateITE]
  split_ifs
  case _ c1 =>
    subst c1
    contradiction
  case _ c1 =>
    rfl
}
State after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
⊢ Holds D I (Function.updateITE V v d) E phi

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
⊢ Holds D I (Function.updateITE V v d) E phi
Tactic:
simp only [s1]
State after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
⊢ Holds D I V E phi

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
⊢ Holds D I V E phi
Tactic:
exact a2
State after:
no goals

State before:
case s1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
⊢ Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
Tactic:
apply Holds_coincide_Var
State after:
case s1.h1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
⊢ ∀ (v_1 : VarName), isFreeIn v_1 phi → Function.updateITE V v d v_1 = V v_1

State before:
case s1.h1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
⊢ ∀ (v_1 : VarName), isFreeIn v_1 phi → Function.updateITE V v d v_1 = V v_1
Tactic:
intro v' a1
State after:
case s1.h1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
⊢ Function.updateITE V v d v' = V v'

State before:
case s1.h1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
⊢ Function.updateITE V v d v' = V v'
Tactic:
simp only [Function.updateITE]
State after:
case s1.h1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
⊢ (if v' = v then d else V v') = V v'

State before:
case s1.h1
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
⊢ (if v' = v then d else V v') = V v'
Tactic:
split_ifs
State after:
case pos
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
h✝ : v' = v
⊢ d = V v'

case neg
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
h✝ : ¬v' = v
⊢ V v' = V v'

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
c1 : v' = v
⊢ d = V v'
Tactic:
case _ c1 =>
  subst c1
  contradiction
State after:
no goals

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
c1 : ¬v' = v
⊢ V v' = V v'
Tactic:
case _ c1 =>
  rfl
State after:
no goals

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
c1 : v' = v
⊢ d = V v'
Tactic:
subst c1
State after:
Δ : List Formula
F phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
ih : ¬isFreeIn v' phi
⊢ d = V v'

State before:
Δ : List Formula
F phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
ih : ¬isFreeIn v' phi
⊢ d = V v'
Tactic:
contradiction
State after:
no goals

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : Holds D I V E phi
d : D
v' : VarName
a1 : isFreeIn v' phi
c1 : ¬v' = v
⊢ V v' = V v'
Tactic:
rfl
State after:
no goals

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
a✝ : IsDeduct [] phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E phi
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (forall_ v phi)
Tactic:
intro D I V E _
State after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
a✝¹ : IsDeduct [] phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (forall_ v phi)

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
a✝¹ : IsDeduct [] phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (forall_ v phi)
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
a✝¹ : IsDeduct [] phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ ∀ (d : D), Holds D I (Function.updateITE V v d) E phi

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
a✝¹ : IsDeduct [] phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ ∀ (d : D), Holds D I (Function.updateITE V v d) E phi
Tactic:
intro d
State after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
a✝¹ : IsDeduct [] phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
d : D
⊢ Holds D I (Function.updateITE V v d) E phi

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
a✝¹ : IsDeduct [] phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
d : D
⊢ Holds D I (Function.updateITE V v d) E phi
Tactic:
apply ih_2
State after:
case a
Δ : List Formula
F : Formula
v : VarName
phi : Formula
a✝¹ : IsDeduct [] phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
d : D
⊢ ∀ H ∈ [], Holds D I (Function.updateITE V v d) E H

State before:
case a
Δ : List Formula
F : Formula
v : VarName
phi : Formula
a✝¹ : IsDeduct [] phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ [], Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
d : D
⊢ ∀ H ∈ [], Holds D I (Function.updateITE V v d) E H
Tactic:
simp
State after:
no goals

State before:
Δ : List Formula
F : Formula
v : VarName
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (eq_ v v)
Tactic:
intro D I V E _
State after:
Δ : List Formula
F : Formula
v : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (eq_ v v)

State before:
Δ : List Formula
F : Formula
v : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (eq_ v v)
Tactic:
simp only [Holds]
State after:
no goals

State before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E (((eq_ x_0 y_0).and_ (eq_ x_1 y_1)).imp_ ((eq_ x_0 x_1).iff_ (eq_ y_0 y_1)))
Tactic:
intro D I V E _
State after:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (((eq_ x_0 y_0).and_ (eq_ x_1 y_1)).imp_ ((eq_ x_0 x_1).iff_ (eq_ y_0 y_1)))

State before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (((eq_ x_0 y_0).and_ (eq_ x_1 y_1)).imp_ ((eq_ x_0 x_1).iff_ (eq_ y_0 y_1)))
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ V x_0 = V y_0 ∧ V x_1 = V y_1 → (V x_0 = V x_1 ↔ V y_0 = V y_1)

State before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ V x_0 = V y_0 ∧ V x_1 = V y_1 → (V x_0 = V x_1 ↔ V y_0 = V y_1)
Tactic:
intro a2
State after:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : V x_0 = V y_0 ∧ V x_1 = V y_1
⊢ V x_0 = V x_1 ↔ V y_0 = V y_1

State before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : V x_0 = V y_0 ∧ V x_1 = V y_1
⊢ V x_0 = V x_1 ↔ V y_0 = V y_1
Tactic:
cases a2
State after:
case intro
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
left✝ : V x_0 = V y_0
right✝ : V x_1 = V y_1
⊢ V x_0 = V x_1 ↔ V y_0 = V y_1

State before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2_left : V x_0 = V y_0
a2_right : V x_1 = V y_1
⊢ V x_0 = V x_1 ↔ V y_0 = V y_1
Tactic:
case _ a2_left a2_right =>
  simp only [a2_left]
  simp only [a2_right]
State after:
no goals

State before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2_left : V x_0 = V y_0
a2_right : V x_1 = V y_1
⊢ V x_0 = V x_1 ↔ V y_0 = V y_1
Tactic:
simp only [a2_left]
State after:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2_left : V x_0 = V y_0
a2_right : V x_1 = V y_1
⊢ V y_0 = V x_1 ↔ V y_0 = V y_1

State before:
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2_left : V x_0 = V y_0
a2_right : V x_1 = V y_1
⊢ V y_0 = V x_1 ↔ V y_0 = V y_1
Tactic:
simp only [a2_right]
State after:
no goals

State before:
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E ((List.foldr and_ true_ (List.zipWith eq_ xs ys)).imp_ ((pred_var_ X xs).iff_ (pred_var_ X ys)))
Tactic:
intro D I V E _
State after:
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((List.foldr and_ true_ (List.zipWith eq_ xs ys)).imp_ ((pred_var_ X xs).iff_ (pred_var_ X ys)))

State before:
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((List.foldr and_ true_ (List.zipWith eq_ xs ys)).imp_ ((pred_var_ X xs).iff_ (pred_var_ X ys)))
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs ys)) →
    (I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V ys))

State before:
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs ys)) →
    (I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V ys))
Tactic:
intro a1
State after:
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs ys))
⊢ I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V ys)

State before:
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs ys))
⊢ I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V ys)
Tactic:
congr! 1
State after:
case a.h.e'_4
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs ys))
⊢ List.map V xs = List.map V ys

State before:
case a.h.e'_4
Δ : List Formula
F : Formula
X : PredName
xs ys : List VarName
ih_1 : xs.length = ys.length
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs ys))
⊢ List.map V xs = List.map V ys
Tactic:
induction xs generalizing ys
State after:
case a.h.e'_4.nil
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ys : List VarName
ih_1 : [].length = ys.length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] ys))
⊢ List.map V [] = List.map V ys

case a.h.e'_4.cons
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
head✝ : VarName
tail✝ : List VarName
tail_ih✝ :
  ∀ (ys : List VarName),
    tail✝.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ tail✝ ys)) → List.map V tail✝ = List.map V ys
ys : List VarName
ih_1 : (head✝ :: tail✝).length = ys.length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (head✝ :: tail✝) ys))
⊢ List.map V (head✝ :: tail✝) = List.map V ys

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ys : List VarName
ih_1 : [].length = ys.length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] ys))
⊢ List.map V [] = List.map V ys
Tactic:
case _ =>
  cases ys
  case _ =>
    simp only [Holds]
  case cons ys_hd ys_tl =>
    simp at ih_1
State after:
no goals

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ys : List VarName
ih_1 : [].length = ys.length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] ys))
⊢ List.map V [] = List.map V ys
Tactic:
cases ys
State after:
case nil
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ih_1 : [].length = [].length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] []))
⊢ List.map V [] = List.map V []

case cons
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
head✝ : VarName
tail✝ : List VarName
ih_1 : [].length = (head✝ :: tail✝).length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] (head✝ :: tail✝)))
⊢ List.map V [] = List.map V (head✝ :: tail✝)

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ih_1 : [].length = [].length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] []))
⊢ List.map V [] = List.map V []
Tactic:
case _ =>
  simp only [Holds]
State after:
no goals

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ys_hd : VarName
ys_tl : List VarName
ih_1 : [].length = (ys_hd :: ys_tl).length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] (ys_hd :: ys_tl)))
⊢ List.map V [] = List.map V (ys_hd :: ys_tl)
Tactic:
case cons ys_hd ys_tl =>
  simp at ih_1
State after:
no goals

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ih_1 : [].length = [].length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] []))
⊢ List.map V [] = List.map V []
Tactic:
simp only [Holds]
State after:
no goals

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
ys_hd : VarName
ys_tl : List VarName
ih_1 : [].length = (ys_hd :: ys_tl).length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ [] (ys_hd :: ys_tl)))
⊢ List.map V [] = List.map V (ys_hd :: ys_tl)
Tactic:
simp at ih_1
State after:
no goals

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys : List VarName
ih_1 : (xs_hd :: xs_tl).length = ys.length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) ys))
⊢ List.map V (xs_hd :: xs_tl) = List.map V ys
Tactic:
cases ys
State after:
case nil
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ih_1 : (xs_hd :: xs_tl).length = [].length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) []))
⊢ List.map V (xs_hd :: xs_tl) = List.map V []

case cons
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
head✝ : VarName
tail✝ : List VarName
ih_1 : (xs_hd :: xs_tl).length = (head✝ :: tail✝).length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) (head✝ :: tail✝)))
⊢ List.map V (xs_hd :: xs_tl) = List.map V (head✝ :: tail✝)

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ih_1 : (xs_hd :: xs_tl).length = [].length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) []))
⊢ List.map V (xs_hd :: xs_tl) = List.map V []
Tactic:
case nil =>
  simp at ih_1
State after:
no goals

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ih_1 : (xs_hd :: xs_tl).length = [].length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) []))
⊢ List.map V (xs_hd :: xs_tl) = List.map V []
Tactic:
simp at ih_1
State after:
no goals

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) (ys_hd :: ys_tl)))
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)
Tactic:
simp at ih_1
State after:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) (ys_hd :: ys_tl)))
ih_1 : xs_tl.length = ys_tl.length
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
a1 : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ (xs_hd :: xs_tl) (ys_hd :: ys_tl)))
ih_1 : xs_tl.length = ys_tl.length
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)
Tactic:
simp at a1
State after:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
a1 : Holds D I V E ((eq_ xs_hd ys_hd).and_ (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl)))
ih_1 : xs_tl.length = ys_tl.length
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
a1 : Holds D I V E ((eq_ xs_hd ys_hd).and_ (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl)))
ih_1 : xs_tl.length = ys_tl.length
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)
Tactic:
simp only [Holds] at a1
State after:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1 : V xs_hd = V ys_hd ∧ Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1 : V xs_hd = V ys_hd ∧ Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)
Tactic:
cases a1
State after:
case intro
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
left✝ : V xs_hd = V ys_hd
right✝ : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1_left : V xs_hd = V ys_hd
a1_right : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ List.map V (xs_hd :: xs_tl) = List.map V (ys_hd :: ys_tl)
Tactic:
simp
State after:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1_left : V xs_hd = V ys_hd
a1_right : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ V xs_hd = V ys_hd ∧ List.map V xs_tl = List.map V ys_tl

State before:
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1_left : V xs_hd = V ys_hd
a1_right : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ V xs_hd = V ys_hd ∧ List.map V xs_tl = List.map V ys_tl
Tactic:
constructor
State after:
case left
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1_left : V xs_hd = V ys_hd
a1_right : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ V xs_hd = V ys_hd

case right
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1_left : V xs_hd = V ys_hd
a1_right : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ List.map V xs_tl = List.map V ys_tl

State before:
case left
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1_left : V xs_hd = V ys_hd
a1_right : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ V xs_hd = V ys_hd
Tactic:
exact a1_left
State after:
no goals

State before:
case right
Δ : List Formula
F : Formula
X : PredName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
xs_hd : VarName
xs_tl : List VarName
xs_ih :
  ∀ (ys : List VarName),
    xs_tl.length = ys.length →
      Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys)) → List.map V xs_tl = List.map V ys
ys_hd : VarName
ys_tl : List VarName
ih_1 : xs_tl.length = ys_tl.length
a1_left : V xs_hd = V ys_hd
a1_right : Holds D I V E (List.foldr and_ true_ (List.zipWith eq_ xs_tl ys_tl))
⊢ List.map V xs_tl = List.map V ys_tl
Tactic:
apply xs_ih ys_tl ih_1 a1_right
State after:
no goals

State before:
Δ : List Formula
F : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (false_.iff_ true_.not_)
Tactic:
intro D I V E _
State after:
Δ : List Formula
F : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (false_.iff_ true_.not_)

State before:
Δ : List Formula
F : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E (false_.iff_ true_.not_)
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ False ↔ ¬True

State before:
Δ : List Formula
F : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ False ↔ ¬True
Tactic:
tauto
State after:
no goals

State before:
Δ : List Formula
F phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi.and_ psi).iff_ (phi.imp_ psi.not_).not_)
Tactic:
intro D I V E _
State after:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((phi.and_ psi).iff_ (phi.imp_ psi.not_).not_)

State before:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((phi.and_ psi).iff_ (phi.imp_ psi.not_).not_)
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E phi ∧ Holds D I V E psi ↔ ¬(Holds D I V E phi → ¬Holds D I V E psi)

State before:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E phi ∧ Holds D I V E psi ↔ ¬(Holds D I V E phi → ¬Holds D I V E psi)
Tactic:
tauto
State after:
no goals

State before:
Δ : List Formula
F phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((phi.or_ psi).iff_ (phi.not_.imp_ psi))
Tactic:
intro D I V E _
State after:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((phi.or_ psi).iff_ (phi.not_.imp_ psi))

State before:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((phi.or_ psi).iff_ (phi.not_.imp_ psi))
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E phi ∨ Holds D I V E psi ↔ ¬Holds D I V E phi → Holds D I V E psi

State before:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E phi ∨ Holds D I V E psi ↔ ¬Holds D I V E phi → Holds D I V E psi
Tactic:
tauto
State after:
no goals

State before:
Δ : List Formula
F phi psi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) →
      Holds D I V E
        (((phi.iff_ psi).imp_ ((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_).imp_
            (((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_.imp_ (phi.iff_ psi)).not_).not_
Tactic:
intro D I V E _
State after:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E
    (((phi.iff_ psi).imp_ ((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_).imp_
        (((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_.imp_ (phi.iff_ psi)).not_).not_

State before:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E
    (((phi.iff_ psi).imp_ ((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_).imp_
        (((phi.imp_ psi).imp_ (psi.imp_ phi).not_).not_.imp_ (phi.iff_ psi)).not_).not_
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ ¬(((Holds D I V E phi ↔ Holds D I V E psi) →
        ¬((Holds D I V E phi → Holds D I V E psi) → ¬(Holds D I V E psi → Holds D I V E phi))) →
      ¬(¬((Holds D I V E phi → Holds D I V E psi) → ¬(Holds D I V E psi → Holds D I V E phi)) →
          (Holds D I V E phi ↔ Holds D I V E psi)))

State before:
Δ : List Formula
F phi psi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ ¬(((Holds D I V E phi ↔ Holds D I V E psi) →
        ¬((Holds D I V E phi → Holds D I V E psi) → ¬(Holds D I V E psi → Holds D I V E phi))) →
      ¬(¬((Holds D I V E phi → Holds D I V E psi) → ¬(Holds D I V E psi → Holds D I V E phi)) →
          (Holds D I V E phi ↔ Holds D I V E psi)))
Tactic:
tauto
State after:
no goals

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E ((exists_ v phi).iff_ (forall_ v phi.not_).not_)
Tactic:
intro D I V E _
State after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((exists_ v phi).iff_ (forall_ v phi.not_).not_)

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ Holds D I V E ((exists_ v phi).iff_ (forall_ v phi.not_).not_)
Tactic:
simp only [Holds]
State after:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (∃ d, Holds D I (Function.updateITE V v d) E phi) ↔ ¬∀ (d : D), ¬Holds D I (Function.updateITE V v d) E phi

State before:
Δ : List Formula
F : Formula
v : VarName
phi : Formula
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
⊢ (∃ d, Holds D I (Function.updateITE V v d) E phi) ↔ ¬∀ (d : D), ¬Holds D I (Function.updateITE V v d) E phi
Tactic:
simp
State after:
no goals

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ List.map (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ) Δ', Holds D I V E H) →
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Tactic:
intro D I V E a1
State after:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ List.map (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ) Δ', Holds D I V E H
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ H ∈ List.map (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ) Δ', Holds D I V E H
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Tactic:
simp at a1
State after:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ a ∈ Δ', Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ a)
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ a ∈ Δ', Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ a)
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Tactic:
obtain s1 := Sub.Pred.All.Rec.Option.Fresh.substitution_theorem D I V E freshChar τ
State after:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ a ∈ Δ', Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ a)
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a1 : ∀ a ∈ Δ', Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ a)
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Tactic:
simp only [← s1] at a1
State after:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
a1 : ∀ a ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E a
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
a1 : ∀ a ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E a
⊢ Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ phi)
Tactic:
simp only [← s1]
State after:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
a1 : ∀ a ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E a
⊢ Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E phi

State before:
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
a1 : ∀ a ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E a
⊢ Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E phi
Tactic:
apply ih_2
State after:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
a1 : ∀ a ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E a
⊢ ∀ H ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E H

State before:
case a
Δ : List Formula
F : Formula
Δ' : List Formula
phi : Formula
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : IsDeduct Δ' phi
ih_2 :
  ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), (∀ H ∈ Δ', Holds D I V E H) → Holds D I V E phi
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
s1 :
  ∀ (F : Formula),
    Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E F ↔
      Holds D I V E (Sub.Pred.All.Rec.Option.Fresh.sub freshChar τ F)
a1 : ∀ a ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E a
⊢ ∀ H ∈ Δ', Holds D (Sub.Pred.All.Rec.Option.Fresh.I' D I V E τ) V E H
Tactic:
exact a1
State after:
no goals