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

State before:
D : Type
I : Interpretation D
V V' : Valuation D
M : MetaValuation D
E : Env
F : Formula
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs F
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M E F ↔ Holds D I V' M E F
Tactic:
induction E generalizing F vs V V'
State after:
case nil
D : Type
I : Interpretation D
M : MetaValuation D
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 [] F ↔ Holds D I V' M [] F

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

State before:
D : Type
I : Interpretation D
M : MetaValuation D
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M [] (def_ X xs) ↔ Holds D I V' M [] (def_ X xs)
Tactic:
case nil.def_ X xs =>
  simp only [Holds]
State after:
no goals

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'
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✝)

State before:
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)
X : MetaVarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (meta_var_ X) ↔ Holds D I V' M (head✝ :: tail✝) (meta_var_ X)
Tactic:
case meta_var_ X =>
  unfold NoMetaVarAndAllFreeInList at h1
  contradiction
State after:
no goals

State before:
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)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (pred_ X xs) ↔ Holds D I V' M (head✝ :: tail✝) (pred_ X xs)
Tactic:
case pred_ X xs =>
  unfold NoMetaVarAndAllFreeInList at h1
  simp only [Holds]
  congr! 1
  simp only [List.map_eq_map_iff]
  tauto
State after:
no goals

State before:
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_
Tactic:
case true_ =>
  simp only [Holds]
State after:
no goals

State before:
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)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi.not_
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) phi.not_ ↔ Holds D I V' M (head✝ :: tail✝) phi.not_
Tactic:
case not_ phi phi_ih =>
  unfold NoMetaVarAndAllFreeInList at h1
  simp only [Holds]
  congr! 1
  exact phi_ih V V' vs h1 h2
State after:
no goals

State before:
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)
X : MetaVarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (meta_var_ X) ↔ Holds D I V' M (head✝ :: tail✝) (meta_var_ X)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
State after:
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)
X : MetaVarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : False
⊢ Holds D I V M (head✝ :: tail✝) (meta_var_ X) ↔ Holds D I V' M (head✝ :: tail✝) (meta_var_ X)

State before:
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)
X : MetaVarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : False
⊢ Holds D I V M (head✝ :: tail✝) (meta_var_ X) ↔ Holds D I V' M (head✝ :: tail✝) (meta_var_ X)
Tactic:
contradiction
State after:
no goals

State before:
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)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (pred_ X xs) ↔ Holds D I V' M (head✝ :: tail✝) (pred_ X xs)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
State after:
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)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ Holds D I V M (head✝ :: tail✝) (pred_ X xs) ↔ Holds D I V' M (head✝ :: tail✝) (pred_ X xs)

State before:
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)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ Holds D I V M (head✝ :: tail✝) (pred_ X xs) ↔ Holds D I V' M (head✝ :: tail✝) (pred_ X xs)
Tactic:
simp only [Holds]
State after:
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)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ I X (List.map V xs) ↔ I X (List.map V' xs)

State before:
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)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ I X (List.map V xs) ↔ I X (List.map V' xs)
Tactic:
congr! 1
State after:
case a.h.e'_2
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)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ List.map V xs = List.map V' xs

State before:
case a.h.e'_2
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)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ List.map V xs = List.map V' xs
Tactic:
simp only [List.map_eq_map_iff]
State after:
case a.h.e'_2
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)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ ∀ x ∈ xs, V x = V' x

State before:
case a.h.e'_2
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)
X : PredName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ ∀ x ∈ xs, V x = V' x
Tactic:
tauto
State after:
no goals

State before:
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)
x y : VarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ x y)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (eq_ x y) ↔ Holds D I V' M (head✝ :: tail✝) (eq_ x y)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
State after:
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)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : x ∈ vs ∧ y ∈ vs
⊢ Holds D I V M (head✝ :: tail✝) (eq_ x y) ↔ Holds D I V' M (head✝ :: tail✝) (eq_ x y)

State before:
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)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : x ∈ vs ∧ y ∈ vs
⊢ Holds D I V M (head✝ :: tail✝) (eq_ x y) ↔ Holds D I V' M (head✝ :: tail✝) (eq_ x y)
Tactic:
cases h1
State after:
case intro
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)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
left✝ : x ∈ vs
right✝ : y ∈ vs
⊢ Holds D I V M (head✝ :: tail✝) (eq_ x y) ↔ Holds D I V' M (head✝ :: tail✝) (eq_ x y)

State before:
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)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ Holds D I V M (head✝ :: tail✝) (eq_ x y) ↔ Holds D I V' M (head✝ :: tail✝) (eq_ x y)
Tactic:
simp only [Holds]
State after:
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)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ V x = V y ↔ V' x = V' y

State before:
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)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ V x = V y ↔ V' x = V' y
Tactic:
congr! 1
State after:
case a.h.e'_2
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)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ V x = V' x

case a.h.e'_3
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)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ V y = V' y

State before:
case a.h.e'_2
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)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ V x = V' x
Tactic:
exact h2 x h1_left
State after:
no goals

State before:
case a.h.e'_3
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)
x y : VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ V y = V' y
Tactic:
exact h2 y h1_right
State after:
no goals

State before:
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_
Tactic:
simp only [Holds]
State after:
no goals

State before:
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)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi.not_
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) phi.not_ ↔ Holds D I V' M (head✝ :: tail✝) phi.not_
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
State after:
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)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ Holds D I V M (head✝ :: tail✝) phi.not_ ↔ Holds D I V' M (head✝ :: tail✝) phi.not_

State before:
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)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ Holds D I V M (head✝ :: tail✝) phi.not_ ↔ Holds D I V' M (head✝ :: tail✝) phi.not_
Tactic:
simp only [Holds]
State after:
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)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ ¬Holds D I V M (head✝ :: tail✝) phi ↔ ¬Holds D I V' M (head✝ :: tail✝) phi

State before:
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)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ ¬Holds D I V M (head✝ :: tail✝) phi ↔ ¬Holds D I V' M (head✝ :: tail✝) phi
Tactic:
congr! 1
State after:
case a.h.e'_1.a
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)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi

State before:
case a.h.e'_1.a
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)
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi
⊢ Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi
Tactic:
exact phi_ih V V' vs h1 h2
State after:
no goals

State before:
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)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (phi.imp_ psi)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (phi.imp_ psi) ↔ Holds D I V' M (head✝ :: tail✝) (phi.imp_ psi)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
State after:
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)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ Holds D I V M (head✝ :: tail✝) (phi.imp_ psi) ↔ Holds D I V' M (head✝ :: tail✝) (phi.imp_ psi)

State before:
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)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ Holds D I V M (head✝ :: tail✝) (phi.imp_ psi) ↔ Holds D I V' M (head✝ :: tail✝) (phi.imp_ psi)
Tactic:
simp only [Holds]
State after:
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)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ Holds D I V M (head✝ :: tail✝) phi → Holds D I V M (head✝ :: tail✝) psi ↔
    Holds D I V' M (head✝ :: tail✝) phi → Holds D I V' M (head✝ :: tail✝) psi

State before:
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)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ Holds D I V M (head✝ :: tail✝) phi → Holds D I V M (head✝ :: tail✝) psi ↔
    Holds D I V' M (head✝ :: tail✝) phi → Holds D I V' M (head✝ :: tail✝) psi
Tactic:
cases h1
State after:
case intro
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)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
left✝ : NoMetaVarAndAllFreeInList vs phi
right✝ : NoMetaVarAndAllFreeInList vs psi
⊢ Holds D I V M (head✝ :: tail✝) phi → Holds D I V M (head✝ :: tail✝) psi ↔
    Holds D I V' M (head✝ :: tail✝) phi → Holds D I V' M (head✝ :: tail✝) psi

State before:
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)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ Holds D I V M (head✝ :: tail✝) phi → Holds D I V M (head✝ :: tail✝) psi ↔
    Holds D I V' M (head✝ :: tail✝) phi → Holds D I V' M (head✝ :: tail✝) psi
Tactic:
congr! 1
State after:
case a.h.a
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)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi

case a.h'.a
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)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
a✝ : Holds D I V' M (head✝ :: tail✝) phi
⊢ Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi

State before:
case a.h.a
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)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi
Tactic:
exact phi_ih V V' vs h1_left h2
State after:
no goals

State before:
case a.h'.a
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)
phi psi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs psi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
a✝ : Holds D I V' M (head✝ :: tail✝) phi
⊢ Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V' M (head✝ :: tail✝) psi
Tactic:
exact psi_ih V V' vs h1_right h2
State after:
no goals

State before:
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (forall_ x phi)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (head✝ :: tail✝) (forall_ x phi) ↔ Holds D I V' M (head✝ :: tail✝) (forall_ x phi)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
State after:
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ Holds D I V M (head✝ :: tail✝) (forall_ x phi) ↔ Holds D I V' M (head✝ :: tail✝) (forall_ x phi)

State before:
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ Holds D I V M (head✝ :: tail✝) (forall_ x phi) ↔ Holds D I V' M (head✝ :: tail✝) (forall_ x phi)
Tactic:
simp only [Holds]
State after:
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ (∀ (d : D), Holds D I (Function.updateITE V x d) M (head✝ :: tail✝) phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V' x d) M (head✝ :: tail✝) phi

State before:
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ (∀ (d : D), Holds D I (Function.updateITE V x d) M (head✝ :: tail✝) phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V' x d) M (head✝ :: tail✝) phi
Tactic:
apply forall_congr'
State after:
case h
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) M (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V' x a) M (head✝ :: tail✝) phi

State before:
case h
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) M (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V' x a) M (head✝ :: tail✝) phi
Tactic:
intro a
State after:
case h
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
⊢ Holds D I (Function.updateITE V x a) M (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V' x a) M (head✝ :: tail✝) phi

State before:
case h
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
⊢ Holds D I (Function.updateITE V x a) M (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V' x a) M (head✝ :: tail✝) phi
Tactic:
apply phi_ih
State after:
case h.h1
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
⊢ NoMetaVarAndAllFreeInList ?h.vs phi

case h.h2
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
⊢ ∀ v ∈ ?h.vs, Function.updateITE V x a v = Function.updateITE V' x a v

case h.vs
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
⊢ List VarName

State before:
case h.h1
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
⊢ NoMetaVarAndAllFreeInList ?h.vs phi
Tactic:
exact h1
State after:
no goals

State before:
case h.h2
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
⊢ ∀ v ∈ x :: vs, Function.updateITE V x a v = Function.updateITE V' x a v
Tactic:
intro v a1
State after:
case h.h2
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
v : VarName
a1 : v ∈ x :: vs
⊢ Function.updateITE V x a v = Function.updateITE V' x a v

State before:
case h.h2
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
v : VarName
a1 : v ∈ x :: vs
⊢ Function.updateITE V x a v = Function.updateITE V' x a v
Tactic:
unfold Function.updateITE
State after:
case h.h2
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
v : VarName
a1 : v ∈ x :: vs
⊢ (if v = x then a else V v) = if v = x then a else V' v

State before:
case h.h2
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
v : VarName
a1 : v ∈ x :: vs
⊢ (if v = x then a else V v) = if v = x then a else V' v
Tactic:
split_ifs
State after:
case pos
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
v : VarName
a1 : v ∈ x :: vs
h✝ : v = x
⊢ a = a

case neg
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
v : VarName
a1 : v ∈ x :: vs
h✝ : ¬v = x
⊢ V v = V' v

State before:
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
v : VarName
a1 : v ∈ x :: vs
c1 : v = x
⊢ a = a
Tactic:
case _ c1 =>
  rfl
State after:
no goals

State before:
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
v : VarName
a1 : v ∈ x :: vs
c1 : ¬v = x
⊢ V v = V' v
Tactic:
case _ c1 =>
  simp at a1
  tauto
State after:
no goals

State before:
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
v : VarName
a1 : v ∈ x :: vs
c1 : v = x
⊢ a = a
Tactic:
rfl
State after:
no goals

State before:
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
v : VarName
a1 : v ∈ x :: vs
c1 : ¬v = x
⊢ V v = V' v
Tactic:
simp at a1
State after:
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
v : VarName
c1 : ¬v = x
a1 : v = x ∨ v ∈ vs
⊢ V v = V' v

State before:
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)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : Valuation D) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs phi →
      (∀ v ∈ vs, V v = V' v) → (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V' M (head✝ :: tail✝) phi)
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
a : D
v : VarName
c1 : ¬v = x
a1 : v = x ∨ v ∈ vs
⊢ V v = V' v
Tactic:
tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M [] (def_ X xs) ↔ Holds D I V' M [] (def_ X xs)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
h2 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V M (E_hd :: E_tl) (def_ X xs) ↔ Holds D I V' M (E_hd :: E_tl) (def_ X xs)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ Holds D I V M (E_hd :: E_tl) (def_ X xs) ↔ Holds D I V' M (E_hd :: E_tl) (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ Holds D I V M (E_hd :: E_tl) (def_ X xs) ↔ Holds D I V' M (E_hd :: E_tl) (def_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ (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 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 xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
⊢ (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 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 xs)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
h✝ : X = E_hd.name ∧ 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

case neg
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V M E_tl (def_ X xs) ↔ Holds D I V' M E_tl (def_ X xs)

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : X = E_hd.name ∧ 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
Tactic:
apply E_ih (Function.updateListITE V E_hd.args (List.map V xs)) (Function.updateListITE V' E_hd.args (List.map V' xs)) E_hd.F E_hd.args E_hd.nf
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : X = E_hd.name ∧ 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

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : X = E_hd.name ∧ 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
Tactic:
intro v a1
State after:
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : X = E_hd.name ∧ 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

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : X = E_hd.name ∧ 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
Tactic:
apply Function.updateListITE_fun_coincide_mem_eq_len
State after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ ∀ v ∈ xs, V v = V' v

case h2
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ v ∈ E_hd.args

case h3
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ E_hd.args.length = xs.length

State before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ ∀ v ∈ xs, V v = V' v
Tactic:
tauto
State after:
no goals

State before:
case h2
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : X = E_hd.name ∧ 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 h3
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.args
⊢ E_hd.args.length = xs.length
Tactic:
tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V M E_tl (def_ X xs) ↔ Holds D I V' M E_tl (def_ X xs)
Tactic:
apply E_ih V V' (def_ X xs) vs
State after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ NoMetaVarAndAllFreeInList vs (def_ X xs)

case h2
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ ∀ v ∈ vs, V v = V' v

State before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ NoMetaVarAndAllFreeInList vs (def_ X xs)
Tactic:
unfold NoMetaVarAndAllFreeInList
State after:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ xs ⊆ vs

State before:
case h1
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ xs ⊆ vs
Tactic:
exact h1
State after:
no goals

State before:
case h2
D : Type
I : Interpretation D
M : MetaValuation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V V' : Valuation D) (F : Formula) (vs : List VarName),
    NoMetaVarAndAllFreeInList vs F → (∀ v ∈ vs, V v = V' v) → (Holds D I V M E_tl F ↔ Holds D I V' M E_tl F)
X : DefName
xs : List VarName
V V' : Valuation D
vs : List VarName
h2 : ∀ v ∈ vs, V v = V' v
h1 : xs ⊆ vs
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ ∀ v ∈ vs, V v = V' v
Tactic:
exact h2
State after:
no goals