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

State before:
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
F : Formula
h1 : IsMetaVarOrAllDefInEnv E F
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E F ↔ Holds D I V M E (sub σ τ F)
Tactic:
induction F generalizing V
State after:
case meta_var_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
a✝ : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ a✝)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ a✝) ↔
    Holds D I V M E (sub σ τ (meta_var_ a✝))

case pred_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
a✝¹ : PredName
a✝ : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (pred_ a✝¹ a✝)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (pred_ a✝¹ a✝) ↔
    Holds D I V M E (sub σ τ (pred_ a✝¹ a✝))

case eq_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
a✝¹ a✝ : VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (eq_ a✝¹ a✝)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (eq_ a✝¹ a✝) ↔
    Holds D I V M E (sub σ τ (eq_ a✝¹ a✝))

case true_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E true_ ↔ Holds D I V M E (sub σ τ true_)

case not_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
a✝ : Formula
a_ih✝ :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E a✝ →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E a✝ ↔ Holds D I V M E (sub σ τ a✝))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E a✝.not_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E a✝.not_ ↔ Holds D I V M E (sub σ τ a✝.not_)

case imp_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E a✝¹ →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E a✝¹ ↔ Holds D I V M E (sub σ τ a✝¹))
a_ih✝ :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E a✝ →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E a✝ ↔ Holds D I V M E (sub σ τ a✝))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (a✝¹.imp_ a✝)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (a✝¹.imp_ a✝) ↔
    Holds D I V M E (sub σ τ (a✝¹.imp_ a✝))

case forall_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E a✝ →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E a✝ ↔ Holds D I V M E (sub σ τ a✝))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (forall_ a✝¹ a✝)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ a✝¹ a✝) ↔
    Holds D I V M E (sub σ τ (forall_ a✝¹ a✝))

case def_
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
a✝¹ : DefName
a✝ : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (def_ a✝¹ a✝)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (def_ a✝¹ a✝) ↔
    Holds D I V M E (sub σ τ (def_ a✝¹ a✝))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔
    Holds D I V M E (sub σ τ (meta_var_ X))
Tactic:
case meta_var_ X =>
  cases h2
  case intro h2_left h2_right =>
    unfold sub
    simp only [Holds]
    simp only [Function.comp.assoc]
    simp only [h2_left]
    simp only [Function.comp_id]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : PredName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (pred_ X xs) ↔
    Holds D I V M E (sub σ τ (pred_ X xs))
Tactic:
case pred_ X xs =>
  unfold sub
  simp only [Holds]
  simp
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x y : VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (eq_ x y) ↔ Holds D I V M E (sub σ τ (eq_ x y))
Tactic:
case eq_ x y =>
  unfold sub
  simp only [Holds]
  simp
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E true_ ↔ Holds D I V M E (sub σ τ true_)
Tactic:
case true_ =>
  unfold sub
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi.not_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi.not_ ↔ Holds D I V M E (sub σ τ phi.not_)
Tactic:
case not_ phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h1
  unfold sub
  simp only [Holds]
  congr! 1
  exact phi_ih V h1
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (forall_ x phi)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))
Tactic:
case forall_ x phi phi_ih =>
  unfold IsMetaVarOrAllDefInEnv at h1
  cases h2
  case intro h2_left h2_right =>
    unfold sub
    simp only [Holds]
    apply forall_congr'
    intro a
    have s1 : Function.updateITE V (σ.val x) a ∘ σ.val = Function.updateITE (V ∘ σ.val) x a
    apply Function.updateITE_comp_right_injective
    apply Instantiation.is_injective
    simp only [← s1]
    exact phi_ih (Function.updateITE V (σ.val x) a) h1
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔
    Holds D I V M E (sub σ τ (meta_var_ X))
Tactic:
cases h2
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
left✝ : ↑σ ∘ σ' = id
right✝ : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔
    Holds D I V M E (sub σ τ (meta_var_ X))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔
    Holds D I V M E (sub σ τ (meta_var_ X))
Tactic:
case intro h2_left h2_right =>
  unfold sub
  simp only [Holds]
  simp only [Function.comp.assoc]
  simp only [h2_left]
  simp only [Function.comp_id]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔
    Holds D I V M E (sub σ τ (meta_var_ X))
Tactic:
unfold sub
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔ Holds D I V M E (τ X)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (meta_var_ X) ↔ Holds D I V M E (τ X)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I ((V ∘ ↑σ) ∘ σ') M E (τ X) ↔ Holds D I V M E (τ X)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I ((V ∘ ↑σ) ∘ σ') M E (τ X) ↔ Holds D I V M E (τ X)
Tactic:
simp only [Function.comp.assoc]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ ∘ σ') M E (τ X) ↔ Holds D I V M E (τ X)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ ∘ σ') M E (τ X) ↔ Holds D I V M E (τ X)
Tactic:
simp only [h2_left]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ id) M E (τ X) ↔ Holds D I V M E (τ X)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
X : MetaVarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ id) M E (τ X) ↔ Holds D I V M E (τ X)
Tactic:
simp only [Function.comp_id]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : PredName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (pred_ X xs) ↔
    Holds D I V M E (sub σ τ (pred_ X xs))
Tactic:
unfold sub
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : PredName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (pred_ X xs) ↔
    Holds D I V M E (pred_ X (List.map (↑σ) xs))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : PredName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (pred_ X xs) ↔
    Holds D I V M E (pred_ X (List.map (↑σ) xs))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : PredName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ I X (List.map (V ∘ ↑σ) xs) ↔ I X (List.map V (List.map (↑σ) xs))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : PredName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ I X (List.map (V ∘ ↑σ) xs) ↔ I X (List.map V (List.map (↑σ) xs))
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x y : VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (eq_ x y) ↔ Holds D I V M E (sub σ τ (eq_ x y))
Tactic:
unfold sub
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x y : VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (eq_ x y) ↔ Holds D I V M E (eq_ (↑σ x) (↑σ y))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x y : VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (eq_ x y) ↔ Holds D I V M E (eq_ (↑σ x) (↑σ y))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x y : VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ (V ∘ ↑σ) x = (V ∘ ↑σ) y ↔ V (↑σ x) = V (↑σ y)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x y : VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ (V ∘ ↑σ) x = (V ∘ ↑σ) y ↔ V (↑σ x) = V (↑σ y)
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E true_ ↔ Holds D I V M E (sub σ τ true_)
Tactic:
unfold sub
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E true_ ↔ Holds D I V M E true_

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E true_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) 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 : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi.not_
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi.not_ ↔ Holds D I V M E (sub σ τ phi.not_)
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi.not_ ↔ Holds D I V M E (sub σ τ phi.not_)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi.not_ ↔ Holds D I V M E (sub σ τ phi.not_)
Tactic:
unfold sub
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi.not_ ↔ Holds D I V M E (sub σ τ phi).not_

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi.not_ ↔ Holds D I V M E (sub σ τ phi).not_
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ ¬Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ ¬Holds D I V M E (sub σ τ phi)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ ¬Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ ¬Holds D I V M E (sub σ τ phi)
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi)

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi)
Tactic:
exact phi_ih V h1
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (phi.imp_ psi)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E (sub σ τ (phi.imp_ psi))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E (sub σ τ (phi.imp_ psi))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E (sub σ τ (phi.imp_ psi))
Tactic:
cases h1
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
left✝ : IsMetaVarOrAllDefInEnv E phi
right✝ : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E (sub σ τ (phi.imp_ psi))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E (sub σ τ (phi.imp_ psi))
Tactic:
unfold sub
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E ((sub σ τ phi).imp_ (sub σ τ psi))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (phi.imp_ psi) ↔
    Holds D I V M E ((sub σ τ phi).imp_ (sub σ τ psi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi →
      Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔
    Holds D I V M E (sub σ τ phi) → Holds D I V M E (sub σ τ psi)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi →
      Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔
    Holds D I V M E (sub σ τ phi) → Holds D I V M E (sub σ τ psi)
Tactic:
congr! 1
State after:
case a.h.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi)

case a.h'.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
a✝ : Holds D I V M E (sub σ τ phi)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi)

State before:
case a.h.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi)
Tactic:
exact phi_ih V h1_left
State after:
no goals

State before:
case a.h'.a
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
psi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E psi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi))
V : Valuation D
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
a✝ : Holds D I V M E (sub σ τ phi)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E psi ↔ Holds D I V M E (sub σ τ psi)
Tactic:
exact psi_ih V h1_right
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (forall_ x phi)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))
Tactic:
cases h2
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
left✝ : ↑σ ∘ σ' = id
right✝ : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))
Tactic:
case intro h2_left h2_right =>
  unfold sub
  simp only [Holds]
  apply forall_congr'
  intro a
  have s1 : Function.updateITE V (σ.val x) a ∘ σ.val = Function.updateITE (V ∘ σ.val) x a
  apply Function.updateITE_comp_right_injective
  apply Instantiation.is_injective
  simp only [← s1]
  exact phi_ih (Function.updateITE V (σ.val x) a) h1
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))
Tactic:
unfold sub
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (forall_ (↑σ x) (sub σ τ phi))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (forall_ (↑σ x) (sub σ τ phi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ (∀ (d : D), Holds D I (Function.updateITE (V ∘ ↑σ) x d) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V (↑σ x) d) M E (sub σ τ phi)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ (∀ (d : D), Holds D I (Function.updateITE (V ∘ ↑σ) x d) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V (↑σ x) d) M E (sub σ τ phi)
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
      Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)

State before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
      Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Tactic:
intro a
State after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)

State before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Tactic:
have s1 : Function.updateITE V (σ.val x) a ∘ σ.val = Function.updateITE (V ∘ σ.val) x a
State after:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
⊢ Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a

case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)

State before:
case s1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
⊢ Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a

case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Tactic:
apply Function.updateITE_comp_right_injective
State after:
case s1.h1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
⊢ Function.Injective ↑σ

case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)

State before:
case s1.h1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
⊢ Function.Injective ↑σ

case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Tactic:
apply Instantiation.is_injective
State after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)

State before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE (V ∘ ↑σ) x a) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Tactic:
simp only [← s1]
State after:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE V (↑σ x) a ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)

State before:
case h
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
a : D
s1 : Function.updateITE V (↑σ x) a ∘ ↑σ = Function.updateITE (V ∘ ↑σ) x a
⊢ Holds D I (Function.updateITE V (↑σ x) a ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔
    Holds D I (Function.updateITE V (↑σ x) a) M E (sub σ τ phi)
Tactic:
exact phi_ih (Function.updateITE V (σ.val x) a) h1
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (def_ X xs) ↔ Holds D I V M E (sub σ τ (def_ X xs))
Tactic:
induction E
State after:
case nil
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv [] (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M [] (τ X')) [] (def_ X xs) ↔
    Holds D I V M [] (sub σ τ (def_ X xs))

case cons
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  IsMetaVarOrAllDefInEnv tail✝ (def_ X xs) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M tail✝ (τ X')) tail✝ (def_ X xs) ↔
      Holds D I V M tail✝ (sub σ τ (def_ X xs)))
h1 : IsMetaVarOrAllDefInEnv (head✝ :: tail✝) (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (head✝ :: tail✝) (τ X')) (head✝ :: tail✝) (def_ X xs) ↔
    Holds D I V M (head✝ :: tail✝) (sub σ τ (def_ X xs))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv [] (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M [] (τ X')) [] (def_ X xs) ↔
    Holds D I V M [] (sub σ τ (def_ X xs))
Tactic:
case nil =>
  unfold IsMetaVarOrAllDefInEnv at h1
  simp at h1
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv [] (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M [] (τ X')) [] (def_ X xs) ↔
    Holds D I V M [] (sub σ τ (def_ X xs))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
h1 : ∃ d ∈ [], X = d.name ∧ xs.length = d.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M [] (τ X')) [] (def_ X xs) ↔
    Holds D I V M [] (sub σ τ (def_ X xs))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
h1 : ∃ d ∈ [], X = d.name ∧ xs.length = d.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M [] (τ X')) [] (def_ X xs) ↔
    Holds D I V M [] (sub σ τ (def_ X xs))
Tactic:
simp at h1
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  IsMetaVarOrAllDefInEnv E_tl (def_ X xs) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) (E_hd :: E_tl) (def_ X xs) ↔
    Holds D I V M (E_hd :: E_tl) (sub σ τ (def_ X xs))
Tactic:
unfold IsMetaVarOrAllDefInEnv at E_ih
State after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) (E_hd :: E_tl) (def_ X xs) ↔
    Holds D I V M (E_hd :: E_tl) (sub σ τ (def_ X xs))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) (E_hd :: E_tl) (def_ X xs) ↔
    Holds D I V M (E_hd :: E_tl) (sub σ τ (def_ X xs))
Tactic:
have s1 : E_hd.F.metaVarSet = ∅ :=
  no_meta_var_imp_meta_var_set_is_empty E_hd.F E_hd.args E_hd.nf
State after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) (E_hd :: E_tl) (def_ X xs) ↔
    Holds D I V M (E_hd :: E_tl) (sub σ τ (def_ X xs))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) (E_hd :: E_tl) (def_ X xs) ↔
    Holds D I V M (E_hd :: E_tl) (sub σ τ (def_ X xs))
Tactic:
unfold sub
State after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) (E_hd :: E_tl) (def_ X xs) ↔
    Holds D I V M (E_hd :: E_tl) (def_ X (List.map (↑σ) xs))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) (E_hd :: E_tl) (def_ X xs) ↔
    Holds D I V M (E_hd :: E_tl) (def_ X (List.map (↑σ) xs))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
        (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F
    else Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ (List.map (↑σ) xs).length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map (↑σ) xs))) M E_tl E_hd.F
    else Holds D I V M E_tl (def_ X (List.map (↑σ) xs))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
        (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F
    else Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ (List.map (↑σ) xs).length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map (↑σ) xs))) M E_tl E_hd.F
    else Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
simp
State after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
        (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F
    else Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
    else Holds D I V M E_tl (def_ X (List.map (↑σ) xs))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
        (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F
    else Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
    else Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F

case neg
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
case _ c1 =>
  unfold IsMetaVarOrAllDefInEnv at h1
  simp at h1
  cases h1
  case inl c2 =>
    contradiction
  case inr c2 =>
    unfold sub at E_ih
    simp only [← E_ih c2]
    apply holds_coincide_meta_var
    unfold Formula.metaVarSet
    simp
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
Tactic:
cases c1
State after:
case intro
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
left✝ : X = E_hd.name
right✝ : xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
Tactic:
have s2 : Holds D I (Function.updateListITE (V ∘ σ.val) E_hd.args (List.map (V ∘ σ.val) xs)) M E_tl E_hd.F ↔ Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ.val) xs)) M E_tl E_hd.F
State after:
case s2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F

D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F

State before:
case s2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F

D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
Tactic:
apply holds_coincide_var D I (Function.updateListITE (V ∘ σ.val) E_hd.args (List.map (V ∘ σ.val) xs)) (Function.updateListITE V E_hd.args (List.map (V ∘ σ.val) xs)) M E_tl E_hd.F E_hd.args E_hd.nf
State after:
case s2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ ∀ v ∈ E_hd.args,
    Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs) v =
      Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs) v

D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F

State before:
case s2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ ∀ v ∈ E_hd.args,
    Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs) v =
      Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs) v

D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
Tactic:
intro v a1
State after:
case s2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs) v =
    Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs) v

D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F

State before:
case s2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs) v =
    Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs) v

D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
Tactic:
apply Function.updateListITE_mem_eq_len
State after:
case s2.h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ v ∈ E_hd.args

case s2.h2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ E_hd.args.length = (List.map (V ∘ ↑σ) xs).length

D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
Tactic:
simp only [← s2]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs))
      (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl E_hd.F ↔
    Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
Tactic:
apply holds_coincide_meta_var_no_meta_var
State after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ E_hd.F.metaVarSet = ∅

State before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
s2 :
  Holds D I (Function.updateListITE (V ∘ ↑σ) E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ ↑σ) xs)) M E_tl E_hd.F
⊢ E_hd.F.metaVarSet = ∅
Tactic:
exact s1
State after:
no goals

State before:
case s2.h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ v ∈ E_hd.args
Tactic:
exact a1
State after:
no goals

State before:
case s2.h2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ E_hd.args.length = (List.map (V ∘ ↑σ) xs).length
Tactic:
simp
State after:
case s2.h2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ E_hd.args.length = xs.length

State before:
case s2.h2
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ E_hd.args.length = xs.length
Tactic:
simp only [c1_right]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
h1 : IsMetaVarOrAllDefInEnv (E_hd :: E_tl) (def_ X xs)
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
unfold IsMetaVarOrAllDefInEnv at h1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
h1 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
h1 : ∃ d ∈ E_hd :: E_tl, X = d.name ∧ xs.length = d.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
simp at h1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
h1 : X = E_hd.name ∧ xs.length = E_hd.args.length ∨ ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
h1 : X = E_hd.name ∧ xs.length = E_hd.args.length ∨ ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
cases h1
State after:
case inl
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))

case inr
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
h✝ : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
case inl c2 =>
  contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
case inr c2 =>
  unfold sub at E_ih
  simp only [← E_ih c2]
  apply holds_coincide_meta_var
  unfold Formula.metaVarSet
  simp
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (sub σ τ (def_ X xs)))
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
unfold sub at E_ih
State after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I V M E_tl (def_ X (List.map (↑σ) xs))
Tactic:
simp only [← E_ih c2]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X')) E_tl (def_ X xs) ↔
    Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs)
Tactic:
apply holds_coincide_meta_var
State after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ ∀ (V' : Valuation D),
    ∀ X_1 ∈ (def_ X xs).metaVarSet, Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X_1) ↔ Holds D I (V' ∘ σ') M E_tl (τ X_1)

State before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ ∀ (V' : Valuation D),
    ∀ X_1 ∈ (def_ X xs).metaVarSet, Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X_1) ↔ Holds D I (V' ∘ σ') M E_tl (τ X_1)
Tactic:
unfold Formula.metaVarSet
State after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ ∀ (V' : Valuation D), ∀ X ∈ ∅, Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X) ↔ Holds D I (V' ∘ σ') M E_tl (τ X)

State before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
h2 : ↑σ ∘ σ' = id ∧ σ' ∘ ↑σ = id
X : DefName
xs : List VarName
V : Valuation D
E_hd : Definition
E_tl : List Definition
s1 : E_hd.F.metaVarSet = ∅
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
c2 : ∃ a ∈ E_tl, X = a.name ∧ xs.length = a.args.length
E_ih :
  (∃ d ∈ E_tl, X = d.name ∧ xs.length = d.args.length) →
    (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E_tl (τ X')) E_tl (def_ X xs) ↔
      Holds D I V M E_tl (def_ X (List.map (↑σ) xs)))
⊢ ∀ (V' : Valuation D), ∀ X ∈ ∅, Holds D I (V' ∘ σ') M (E_hd :: E_tl) (τ X) ↔ Holds D I (V' ∘ σ') M E_tl (τ X)
Tactic:
simp
State after:
no goals