Theorem: FOL.NV.Holds_coincide_Env (FOL/NV/Semantics.lean)

State before:
D : Type
I : Interpretation D
V : VarAssignment D
E E' : Env
F : Formula
h1 : ∃ E1, E' = E1 ++ E
h2 : all_def_in_env E F
h3 : E'.nodup_
⊢ Holds D I V E' F ↔ Holds D I V E F
Tactic:
induction F generalizing V
State after:
case pred_const_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
h2 : all_def_in_env E (pred_const_ a✝¹ a✝)
⊢ Holds D I V E' (pred_const_ a✝¹ a✝) ↔ Holds D I V E (pred_const_ a✝¹ a✝)

case pred_var_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
h2 : all_def_in_env E (pred_var_ a✝¹ a✝)
⊢ Holds D I V E' (pred_var_ a✝¹ a✝) ↔ Holds D I V E (pred_var_ a✝¹ a✝)

case eq_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ a✝ : VarName
V : VarAssignment D
h2 : all_def_in_env E (eq_ a✝¹ a✝)
⊢ Holds D I V E' (eq_ a✝¹ a✝) ↔ Holds D I V E (eq_ a✝¹ a✝)

case true_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
V : VarAssignment D
h2 : all_def_in_env E true_
⊢ Holds D I V E' true_ ↔ Holds D I V E true_

case false_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
V : VarAssignment D
h2 : all_def_in_env E false_
⊢ Holds D I V E' false_ ↔ Holds D I V E false_

case not_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝.not_
⊢ Holds D I V E' a✝.not_ ↔ Holds D I V E a✝.not_

case imp_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D), all_def_in_env E a✝¹ → (Holds D I V E' a✝¹ ↔ Holds D I V E a✝¹)
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E (a✝¹.imp_ a✝)
⊢ Holds D I V E' (a✝¹.imp_ a✝) ↔ Holds D I V E (a✝¹.imp_ a✝)

case and_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D), all_def_in_env E a✝¹ → (Holds D I V E' a✝¹ ↔ Holds D I V E a✝¹)
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E (a✝¹.and_ a✝)
⊢ Holds D I V E' (a✝¹.and_ a✝) ↔ Holds D I V E (a✝¹.and_ a✝)

case or_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D), all_def_in_env E a✝¹ → (Holds D I V E' a✝¹ ↔ Holds D I V E a✝¹)
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E (a✝¹.or_ a✝)
⊢ Holds D I V E' (a✝¹.or_ a✝) ↔ Holds D I V E (a✝¹.or_ a✝)

case iff_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D), all_def_in_env E a✝¹ → (Holds D I V E' a✝¹ ↔ Holds D I V E a✝¹)
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E (a✝¹.iff_ a✝)
⊢ Holds D I V E' (a✝¹.iff_ a✝) ↔ Holds D I V E (a✝¹.iff_ a✝)

case forall_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E (forall_ a✝¹ a✝)
⊢ Holds D I V E' (forall_ a✝¹ a✝) ↔ Holds D I V E (forall_ a✝¹ a✝)

case exists_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E (exists_ a✝¹ a✝)
⊢ Holds D I V E' (exists_ a✝¹ a✝) ↔ Holds D I V E (exists_ a✝¹ a✝)

case def_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ a✝¹ a✝)
⊢ Holds D I V E' (def_ a✝¹ a✝) ↔ Holds D I V E (def_ a✝¹ a✝)

State before:
case pred_const_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
h2 : all_def_in_env E (pred_const_ a✝¹ a✝)
⊢ Holds D I V E' (pred_const_ a✝¹ a✝) ↔ Holds D I V E (pred_const_ a✝¹ a✝)

case pred_var_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
h2 : all_def_in_env E (pred_var_ a✝¹ a✝)
⊢ Holds D I V E' (pred_var_ a✝¹ a✝) ↔ Holds D I V E (pred_var_ a✝¹ a✝)

case eq_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ a✝ : VarName
V : VarAssignment D
h2 : all_def_in_env E (eq_ a✝¹ a✝)
⊢ Holds D I V E' (eq_ a✝¹ a✝) ↔ Holds D I V E (eq_ a✝¹ a✝)

case true_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
V : VarAssignment D
h2 : all_def_in_env E true_
⊢ Holds D I V E' true_ ↔ Holds D I V E true_

case false_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
V : VarAssignment D
h2 : all_def_in_env E false_
⊢ Holds D I V E' false_ ↔ Holds D I V E false_

case not_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝.not_
⊢ Holds D I V E' a✝.not_ ↔ Holds D I V E a✝.not_

case imp_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D), all_def_in_env E a✝¹ → (Holds D I V E' a✝¹ ↔ Holds D I V E a✝¹)
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E (a✝¹.imp_ a✝)
⊢ Holds D I V E' (a✝¹.imp_ a✝) ↔ Holds D I V E (a✝¹.imp_ a✝)

case and_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D), all_def_in_env E a✝¹ → (Holds D I V E' a✝¹ ↔ Holds D I V E a✝¹)
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E (a✝¹.and_ a✝)
⊢ Holds D I V E' (a✝¹.and_ a✝) ↔ Holds D I V E (a✝¹.and_ a✝)

case or_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D), all_def_in_env E a✝¹ → (Holds D I V E' a✝¹ ↔ Holds D I V E a✝¹)
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E (a✝¹.or_ a✝)
⊢ Holds D I V E' (a✝¹.or_ a✝) ↔ Holds D I V E (a✝¹.or_ a✝)

case iff_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D), all_def_in_env E a✝¹ → (Holds D I V E' a✝¹ ↔ Holds D I V E a✝¹)
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E (a✝¹.iff_ a✝)
⊢ Holds D I V E' (a✝¹.iff_ a✝) ↔ Holds D I V E (a✝¹.iff_ a✝)

case forall_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E (forall_ a✝¹ a✝)
⊢ Holds D I V E' (forall_ a✝¹ a✝) ↔ Holds D I V E (forall_ a✝¹ a✝)

case exists_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E (exists_ a✝¹ a✝)
⊢ Holds D I V E' (exists_ a✝¹ a✝) ↔ Holds D I V E (exists_ a✝¹ a✝)

case def_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ a✝¹ a✝)
⊢ Holds D I V E' (def_ a✝¹ a✝) ↔ Holds D I V E (def_ a✝¹ a✝)
Tactic:
any_goals
  simp only [all_def_in_env] at h2
  simp only [Holds]
State after:
case not_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝
⊢ ¬Holds D I V E' a✝ ↔ ¬Holds D I V E a✝

case imp_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D), all_def_in_env E a✝¹ → (Holds D I V E' a✝¹ ↔ Holds D I V E a✝¹)
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝¹ ∧ all_def_in_env E a✝
⊢ Holds D I V E' a✝¹ → Holds D I V E' a✝ ↔ Holds D I V E a✝¹ → Holds D I V E a✝

case and_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D), all_def_in_env E a✝¹ → (Holds D I V E' a✝¹ ↔ Holds D I V E a✝¹)
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝¹ ∧ all_def_in_env E a✝
⊢ Holds D I V E' a✝¹ ∧ Holds D I V E' a✝ ↔ Holds D I V E a✝¹ ∧ Holds D I V E a✝

case or_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D), all_def_in_env E a✝¹ → (Holds D I V E' a✝¹ ↔ Holds D I V E a✝¹)
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝¹ ∧ all_def_in_env E a✝
⊢ Holds D I V E' a✝¹ ∨ Holds D I V E' a✝ ↔ Holds D I V E a✝¹ ∨ Holds D I V E a✝

case iff_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D), all_def_in_env E a✝¹ → (Holds D I V E' a✝¹ ↔ Holds D I V E a✝¹)
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝¹ ∧ all_def_in_env E a✝
⊢ (Holds D I V E' a✝¹ ↔ Holds D I V E' a✝) ↔ (Holds D I V E a✝¹ ↔ Holds D I V E a✝)

case forall_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝
⊢ (∀ (d : D), Holds D I (Function.updateITE V a✝¹ d) E' a✝) ↔ ∀ (d : D), Holds D I (Function.updateITE V a✝¹ d) E a✝

case exists_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝
⊢ (∃ d, Holds D I (Function.updateITE V a✝¹ d) E' a✝) ↔ ∃ d, Holds D I (Function.updateITE V a✝¹ d) E a✝

case def_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ a✝¹ a✝)
⊢ Holds D I V E' (def_ a✝¹ a✝) ↔ Holds D I V E (def_ a✝¹ a✝)

State before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ ¬Holds D I V E' phi ↔ ¬Holds D I V E phi
Tactic:
case not_ phi phi_ih =>
  congr! 1
  exact phi_ih V h2
State after:
no goals

State before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ (∃ d, Holds D I (Function.updateITE V x d) E' phi) ↔ ∃ d, Holds D I (Function.updateITE V x d) E phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  first | apply forall_congr' | apply exists_congr
  intro d
  apply phi_ih
  exact h2
State after:
no goals

State before:
case def_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ a✝¹ a✝)
⊢ Holds D I V E' (def_ a✝¹ a✝) ↔ Holds D I V E (def_ a✝¹ a✝)
Tactic:
simp only [all_def_in_env] at h2
State after:
case def_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, a✝¹ = d.name ∧ a✝.length = d.args.length
⊢ Holds D I V E' (def_ a✝¹ a✝) ↔ Holds D I V E (def_ a✝¹ a✝)

State before:
case exists_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝
⊢ Holds D I V E' (exists_ a✝¹ a✝) ↔ Holds D I V E (exists_ a✝¹ a✝)
Tactic:
simp only [Holds]
State after:
case exists_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝
⊢ (∃ d, Holds D I (Function.updateITE V a✝¹ d) E' a✝) ↔ ∃ d, Holds D I (Function.updateITE V a✝¹ d) E a✝

State before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ ¬Holds D I V E' phi ↔ ¬Holds D I V E phi
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ Holds D I V E' phi ↔ Holds D I V E phi

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ Holds D I V E' phi ↔ Holds D I V E phi
Tactic:
exact phi_ih V h2
State after:
no goals

State before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2 : all_def_in_env E phi ∧ all_def_in_env E psi
⊢ (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:
cases h2
State after:
case intro
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
left✝ : all_def_in_env E phi
right✝ : all_def_in_env E psi
⊢ (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:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2_left : all_def_in_env E phi
h2_right : all_def_in_env E psi
⊢ (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:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2_left : all_def_in_env E phi
h2_right : all_def_in_env E psi
⊢ Holds D I V E' phi ↔ Holds D I V E phi

case a.h.e'_2.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2_left : all_def_in_env E phi
h2_right : all_def_in_env E psi
⊢ Holds D I V E' psi ↔ Holds D I V E psi

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2_left : all_def_in_env E phi
h2_right : all_def_in_env E psi
⊢ Holds D I V E' phi ↔ Holds D I V E phi
Tactic:
exact phi_ih V h2_left
State after:
no goals

State before:
case a.h.e'_2.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2_left : all_def_in_env E phi
h2_right : all_def_in_env E psi
⊢ Holds D I V E' psi ↔ Holds D I V E psi
Tactic:
exact psi_ih V h2_right
State after:
no goals

State before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ (∃ d, Holds D I (Function.updateITE V x d) E' phi) ↔ ∃ d, Holds D I (Function.updateITE V x d) E phi
Tactic:
first | apply forall_congr' | apply exists_congr
State after:
case h
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ ∀ (a : D), Holds D I (Function.updateITE V x a) E' phi ↔ Holds D I (Function.updateITE V x a) E phi

State before:
case h
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ ∀ (a : D), Holds D I (Function.updateITE V x a) E' phi ↔ Holds D I (Function.updateITE V x a) E phi
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
d : D
⊢ Holds D I (Function.updateITE V x d) E' phi ↔ Holds D I (Function.updateITE V x d) E phi

State before:
case h
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
d : D
⊢ Holds D I (Function.updateITE V x d) E' phi ↔ Holds D I (Function.updateITE V x d) E phi
Tactic:
apply phi_ih
State after:
case h.h2
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
d : D
⊢ all_def_in_env E phi

State before:
case h.h2
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
d : D
⊢ all_def_in_env E phi
Tactic:
exact h2
State after:
no goals

State before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ (∀ (d : D), Holds D I (Function.updateITE V x d) E' phi) ↔ ∀ (d : D), Holds D I (Function.updateITE V x d) E phi
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ ∀ (a : D), Holds D I (Function.updateITE V x a) E' phi ↔ Holds D I (Function.updateITE V x a) E phi

State before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ (∃ d, Holds D I (Function.updateITE V x d) E' phi) ↔ ∃ d, Holds D I (Function.updateITE V x d) E phi
Tactic:
apply exists_congr
State after:
case h
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ ∀ (a : D), Holds D I (Function.updateITE V x a) E' phi ↔ Holds D I (Function.updateITE V x a) E phi

State before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
apply Exists.elim h1
State after:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
⊢ ∀ (a : Env), E' = a ++ E → (Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs))

State before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
⊢ ∀ (a : Env), E' = a ++ E → (Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs))
Tactic:
intro E1 h1_1
State after:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
clear h1
State after:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : all_def_in_env E (def_ X xs)
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
simp only [all_def_in_env] at h2
State after:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
apply Exists.elim h2
State after:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E
⊢ ∀ (a : Definition),
    a ∈ E ∧ X = a.name ∧ xs.length = a.args.length → (Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs))

State before:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E
⊢ ∀ (a : Definition),
    a ∈ E ∧ X = a.name ∧ xs.length = a.args.length → (Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs))
Tactic:
intro a h2_1
State after:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
clear h2
State after:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E E' : Env
h3 : E'.nodup_
X : DefName
xs : List VarName
V : VarAssignment D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
simp only [Env.nodup_] at h3
State after:
D : Type
I : Interpretation D
E E' : Env
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) E'
X : DefName
xs : List VarName
V : VarAssignment D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E E' : Env
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) E'
X : DefName
xs : List VarName
V : VarAssignment D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V E' (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
subst h1_1
State after:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
E1 : Env
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1 ++ E)
⊢ Holds D I V (E1 ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
E1 : Env
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1 ++ E)
⊢ Holds D I V (E1 ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
induction E1
State after:
case nil
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) ([] ++ E)
⊢ Holds D I V ([] ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)

case cons
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (tail✝ ++ E) →
    (Holds D I V (tail✝ ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (head✝ :: tail✝ ++ E)
⊢ Holds D I V (head✝ :: tail✝ ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) ([] ++ E)
⊢ Holds D I V ([] ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
case nil =>
  simp
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) ([] ++ E)
⊢ Holds D I V ([] ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h3 : List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_hd :: E1_tl ++ E)
⊢ Holds D I V (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
simp at h3
State after:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h3 :
  (∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length) ∧
    List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ Holds D I V (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h3 :
  (∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length) ∧
    List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ Holds D I V (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
cases h2_1
State after:
case intro
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h3 :
  (∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length) ∧
    List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
left✝ : a ∈ E
right✝ : X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h3 :
  (∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length) ∧
    List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
h2_1_left : a ∈ E
h2_1_right : X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
cases h2_1_right
State after:
case intro
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h3 :
  (∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length) ∧
    List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
h2_1_left : a ∈ E
left✝ : X = a.name
right✝ : xs.length = a.args.length
⊢ Holds D I V (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h3 :
  (∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length) ∧
    List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
⊢ Holds D I V (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
cases h3
State after:
case intro
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
left✝ : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
right✝ : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ Holds D I V (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ Holds D I V (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
simp
State after:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ Holds D I V (E1_hd :: (E1_tl ++ E)) (def_ X xs) ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ Holds D I V (E1_hd :: (E1_tl ++ E)) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ (if X = E1_hd.name ∧ xs.length = E1_hd.args.length then
      Holds D I (Function.updateListITE V E1_hd.args (List.map V xs)) (E1_tl ++ E) E1_hd.q
    else Holds D I V (E1_tl ++ E) (def_ X xs)) ↔
    Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ (if X = E1_hd.name ∧ xs.length = E1_hd.args.length then
      Holds D I (Function.updateListITE V E1_hd.args (List.map V xs)) (E1_tl ++ E) E1_hd.q
    else Holds D I V (E1_tl ++ E) (def_ X xs)) ↔
    Holds D I V E (def_ X xs)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
h✝ : X = E1_hd.name ∧ xs.length = E1_hd.args.length
⊢ Holds D I (Function.updateListITE V E1_hd.args (List.map V xs)) (E1_tl ++ E) E1_hd.q ↔ Holds D I V E (def_ X xs)

case neg
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
h✝ : ¬(X = E1_hd.name ∧ xs.length = E1_hd.args.length)
⊢ Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1 : ¬(X = E1_hd.name ∧ xs.length = E1_hd.args.length)
⊢ Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
case _ c1 =>
  exact E1_ih h3_right
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1 : X = E1_hd.name ∧ xs.length = E1_hd.args.length
⊢ Holds D I (Function.updateListITE V E1_hd.args (List.map V xs)) (E1_tl ++ E) E1_hd.q ↔ Holds D I V E (def_ X xs)
Tactic:
cases c1
State after:
case intro
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
left✝ : X = E1_hd.name
right✝ : xs.length = E1_hd.args.length
⊢ Holds D I (Function.updateListITE V E1_hd.args (List.map V xs)) (E1_tl ++ E) E1_hd.q ↔ Holds D I V E (def_ X xs)

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ Holds D I (Function.updateListITE V E1_hd.args (List.map V xs)) (E1_tl ++ E) E1_hd.q ↔ Holds D I V E (def_ X xs)
Tactic:
exfalso
State after:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ False

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ False
Tactic:
apply h3_left a
State after:
case a
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ a ∈ E1_tl ∨ a ∈ E

case a
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.name = a.name

case a
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.args.length = a.args.length

State before:
case a
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ a ∈ E1_tl ∨ a ∈ E
Tactic:
right
State after:
case a.h
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ a ∈ E

State before:
case a.h
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ a ∈ E
Tactic:
exact h2_1_left
State after:
no goals

State before:
case a
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.name = a.name
Tactic:
subst c1_left
State after:
case a
D : Type
I : Interpretation D
E : Env
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
h2_1_left : a ∈ E
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_right : xs.length = E1_hd.args.length
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ E1_hd.name xs) ↔ Holds D I V E (def_ E1_hd.name xs))
h2_1_right_left : E1_hd.name = a.name
⊢ E1_hd.name = a.name

State before:
case a
D : Type
I : Interpretation D
E : Env
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
h2_1_left : a ∈ E
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_right : xs.length = E1_hd.args.length
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ E1_hd.name xs) ↔ Holds D I V E (def_ E1_hd.name xs))
h2_1_right_left : E1_hd.name = a.name
⊢ E1_hd.name = a.name
Tactic:
exact h2_1_right_left
State after:
no goals

State before:
case a
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.args.length = a.args.length
Tactic:
trans List.length xs
State after:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.args.length = xs.length

D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ xs.length = a.args.length

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ E1_hd.args.length = xs.length
Tactic:
simp only [eq_comm]
State after:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ xs.length = E1_hd.args.length

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ xs.length = E1_hd.args.length
Tactic:
exact c1_right
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1_left : X = E1_hd.name
c1_right : xs.length = E1_hd.args.length
⊢ xs.length = a.args.length
Tactic:
exact h2_1_right_right
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
c1 : ¬(X = E1_hd.name ∧ xs.length = E1_hd.args.length)
⊢ Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs)
Tactic:
exact E1_ih h3_right
State after:
no goals