Theorem: MM0.holds_coincide_var
Proof state before:
case cons
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
V V' : Valuation D
F : Formula
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs F
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) F ↔ Holds D I V' M (head✝ :: tail✝) F
Tactic:
induction F generalizing vs V V'
Proof state after:
case cons.meta_var_
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
a✝ : MetaVarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ a✝)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (meta_var_ a✝) ↔ Holds D I V' M (head✝ :: tail✝) (meta_var_ a✝)

case cons.pred_
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
a✝¹ : PredName
a✝ : List VarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ a✝¹ a✝)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (pred_ a✝¹ a✝) ↔ Holds D I V' M (head✝ :: tail✝) (pred_ a✝¹ a✝)

case cons.eq_
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
a✝¹ a✝ : VarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ a✝¹ a✝)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (eq_ a✝¹ a✝) ↔ Holds D I V' M (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.true_
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) true_ ↔ Holds D I V' M (head✝ :: tail✝) true_

case cons.not_
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
a✝ : Formula
a_ih✝ :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs a✝ →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) a✝ ↔ Holds D I V' M (head✝ :: tail✝) a✝)
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs a✝.not_
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) a✝.not_ ↔ Holds D I V' M (head✝ :: tail✝) a✝.not_

case cons.imp_
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs a✝¹ →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) a✝¹ ↔ Holds D I V' M (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs a✝ →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) a✝ ↔ Holds D I V' M (head✝ :: tail✝) a✝)
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (a✝¹.imp_ a✝)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (a✝¹.imp_ a✝) ↔ Holds D I V' M (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.forall_
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs a✝ →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) a✝ ↔ Holds D I V' M (head✝ :: tail✝) a✝)
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (forall_ a✝¹ a✝)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (forall_ a✝¹ a✝) ↔ Holds D I V' M (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.def_
D : Type
I : Interpretation D
M : MetaValuation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M tail✝ F ↔ Holds D I V' M tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ a✝¹ a✝)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I V' M (head✝ :: tail✝) (def_ a✝¹ a✝)