Theorem: MM0.holds_coincide_env (FOL/MM0/MM0.lean)

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
E E' : Env
F : Formula
h1 : ∃ E1, E' = E1 ++ E
h2 : IsMetaVarOrAllDefInEnv E F
h3 : E'.Nodup
⊢ Holds D I V M E' F ↔ Holds D I V M E F
Tactic:
induction F generalizing V
State after:
case meta_var_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝ : MetaVarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (meta_var_ a✝)
⊢ Holds D I V M E' (meta_var_ a✝) ↔ Holds D I V M E (meta_var_ a✝)

case pred_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝¹ : PredName
a✝ : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (pred_ a✝¹ a✝)
⊢ Holds D I V M E' (pred_ a✝¹ a✝) ↔ Holds D I V M E (pred_ a✝¹ a✝)

case eq_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝¹ a✝ : VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (eq_ a✝¹ a✝)
⊢ Holds D I V M E' (eq_ a✝¹ a✝) ↔ Holds D I V M E (eq_ a✝¹ a✝)

case true_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I V M E' true_ ↔ Holds D I V M E true_

case not_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝ : Formula
a_ih✝ : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E a✝ → (Holds D I V M E' a✝ ↔ Holds D I V M E a✝)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E a✝.not_
⊢ Holds D I V M E' a✝.not_ ↔ Holds D I V M E a✝.not_

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

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

case def_
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
a✝¹ : DefName
a✝ : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (def_ a✝¹ a✝)
⊢ Holds D I V M E' (def_ a✝¹ a✝) ↔ Holds D I V M E (def_ a✝¹ a✝)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
X : MetaVarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ Holds D I V M E' (meta_var_ X) ↔ Holds D I V M E (meta_var_ X)
Tactic:
case meta_var_ X =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
X : PredName
xs : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ Holds D I V M E' (pred_ X xs) ↔ Holds D I V M E (pred_ X xs)
Tactic:
case pred_ X xs =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x y : VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ Holds D I V M E' (eq_ x y) ↔ Holds D I V M E (eq_ x y)
Tactic:
case eq_ x y =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I V M E' true_ ↔ Holds D I V M E true_
Tactic:
case true_ =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi.not_
⊢ Holds D I V M E' phi.not_ ↔ Holds D I V M E phi.not_
Tactic:
case not_ phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h2
  simp only [Holds]
  congr! 1
  exact phi_ih V h2
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (forall_ x phi)
⊢ Holds D I V M E' (forall_ x phi) ↔ Holds D I V M E (forall_ x phi)
Tactic:
case forall_ x phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h2
  simp only [Holds]
  apply forall_congr'
  intro a
  exact phi_ih (Function.updateITE V x a) h2
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
X : MetaVarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ Holds D I V M E' (meta_var_ X) ↔ Holds D I V M E (meta_var_ X)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
X : PredName
xs : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ Holds D I V M E' (pred_ X xs) ↔ Holds D I V M E (pred_ X xs)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x y : VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ Holds D I V M E' (eq_ x y) ↔ Holds D I V M E (eq_ x y)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I V M E' true_ ↔ Holds D I V M E true_
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi.not_
⊢ Holds D I V M E' phi.not_ ↔ Holds D I V M E phi.not_
Tactic:
unfold IsMetaVarOrAllDefInEnv at h2
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I V M E' phi.not_ ↔ Holds D I V M E phi.not_

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I V M E' phi.not_ ↔ Holds D I V M E phi.not_
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ ¬Holds D I V M E' phi ↔ ¬Holds D I V M E phi

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

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

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (phi.imp_ psi)
⊢ Holds D I V M E' (phi.imp_ psi) ↔ Holds D I V M E (phi.imp_ psi)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h2
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' (phi.imp_ psi) ↔ Holds D I V M E (phi.imp_ psi)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' (phi.imp_ psi) ↔ Holds D I V M E (phi.imp_ psi)
Tactic:
cases h2
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
left✝ : IsMetaVarOrAllDefInEnv E phi
right✝ : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' (phi.imp_ psi) ↔ Holds D I V M E (phi.imp_ psi)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' (phi.imp_ psi) ↔ Holds D I V M E (phi.imp_ psi)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' phi → Holds D I V M E' psi ↔ Holds D I V M E phi → Holds D I V M E psi

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' phi → Holds D I V M E' psi ↔ Holds D I V M E phi → Holds D I V M E psi
Tactic:
congr! 1
State after:
case a.h.a
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I V M E' phi ↔ Holds D I V M E phi

case a.h'.a
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
a✝ : Holds D I V M E phi
⊢ Holds D I V M E' psi ↔ Holds D I V M E psi

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

State before:
case a.h'.a
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
phi psi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
psi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E psi → (Holds D I V M E' psi ↔ Holds D I V M E psi)
V : Valuation D
h2_left : IsMetaVarOrAllDefInEnv E phi
h2_right : IsMetaVarOrAllDefInEnv E psi
a✝ : Holds D I V M E phi
⊢ Holds D I V M E' psi ↔ Holds D I V M E psi
Tactic:
exact psi_ih V h2_right
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (forall_ x phi)
⊢ Holds D I V M E' (forall_ x phi) ↔ Holds D I V M E (forall_ x phi)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h2
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I V M E' (forall_ x phi) ↔ Holds D I V M E (forall_ x phi)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I V M E' (forall_ x phi) ↔ Holds D I V M E (forall_ x phi)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
⊢ (∀ (d : D), Holds D I (Function.updateITE V x d) M E' phi) ↔ ∀ (d : D), Holds D I (Function.updateITE V x d) M E phi

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

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

State before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.Nodup
x : VarName
phi : Formula
phi_ih : ∀ (V : Valuation D), IsMetaVarOrAllDefInEnv E phi → (Holds D I V M E' phi ↔ Holds D I V M E phi)
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E phi
a : D
⊢ Holds D I (Function.updateITE V x a) M E' phi ↔ Holds D I (Function.updateITE V x a) M E phi
Tactic:
exact phi_ih (Function.updateITE V x a) h2
State after:
no goals

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

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

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

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
h2 : IsMetaVarOrAllDefInEnv E (def_ X xs)
E1 : Env
h1_1 : E' = E1 ++ E
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h2
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)

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

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

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
h2 : ∃ d ∈ E, X = d.name ∧ xs.length = d.args.length
a : Definition
h2_1 : a ∈ E ∧ X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
clear h2
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation 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 M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E E' : Env
h3 : E'.Nodup
X : DefName
xs : List VarName
V : Valuation 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 M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
unfold Env.Nodup at h3
State after:
D : Type
I : Interpretation D
M : MetaValuation 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 : Valuation 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 M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation 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 : Valuation 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 M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
cases h2_1
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation 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 : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
left✝ : a ∈ E
right✝ : X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation 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 : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1_left : a ∈ E
h2_1_right : X = a.name ∧ xs.length = a.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
cases h2_1_right
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation 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 : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
h2_1_left : a ∈ E
left✝ : X = a.name
right✝ : xs.length = a.args.length
⊢ Holds D I V M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation 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 : Valuation D
E1 : Env
h1_1 : E' = E1 ++ E
a : Definition
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 M E' (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
subst h1_1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
E1 : Env
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1 ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
E1 : Env
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1 ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
induction E1
State after:
case nil
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M ([] ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)

case cons
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (tail✝ ++ E) (def_ X xs) ↔ Holds D I V M 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 M (head✝ :: tail✝ ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M ([] ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
case nil =>
  simp
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M ([] ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M 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 M (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
simp at h3
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M 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 M (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M 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 M (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
cases h3
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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 M (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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 M (E1_hd :: E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
simp
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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 M (E1_hd :: (E1_tl ++ E)) (def_ X xs) ↔ Holds D I V M E (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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 M (E1_hd :: (E1_tl ++ E)) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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)) M (E1_tl ++ E) E1_hd.F
    else Holds D I V M (E1_tl ++ E) (def_ X xs)) ↔
    Holds D I V M E (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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)) M (E1_tl ++ E) E1_hd.F
    else Holds D I V M (E1_tl ++ E) (def_ X xs)) ↔
    Holds D I V M E (def_ X xs)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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)) M (E1_tl ++ E) E1_hd.F ↔ Holds D I V M E (def_ X xs)

case neg
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
case _ c1 =>
  exact E1_ih h3_right
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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)) M (E1_tl ++ E) E1_hd.F ↔ Holds D I V M E (def_ X xs)
Tactic:
cases c1
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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)) M (E1_tl ++ E) E1_hd.F ↔ Holds D I V M E (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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)) M (E1_tl ++ E) E1_hd.F ↔ Holds D I V M E (def_ X xs)
Tactic:
exfalso
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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:
simp only [← h2_1_right_left]
State after:
case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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 = X

State before:
case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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 = X
Tactic:
simp only [c1_left]
State after:
no goals

State before:
case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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:
simp only [← h2_1_right_right]
State after:
case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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

State before:
case a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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 [c1_right]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
X : DefName
xs : List VarName
V : Valuation D
a : Definition
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : 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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs))
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 M (E1_tl ++ E) (def_ X xs) ↔ Holds D I V M E (def_ X xs)
Tactic:
exact E1_ih h3_right
State after:
no goals