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

State before:
D : Type
I : Interpretation D
V : Valuation D
M M' : MetaValuation D
E : Env
F : Formula
h1 : ∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M E F ↔ Holds D I V M' E F
Tactic:
induction E generalizing F V M M'
State after:
case nil
D : Type
I : Interpretation D
V : Valuation D
M M' : MetaValuation D
F : Formula
h1 : ∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M [] F ↔ Holds D I V M' [] F

case cons
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
V : Valuation D
M M' : MetaValuation D
F : Formula
h1 : ∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M (head✝ :: tail✝) F ↔ Holds D I V M' (head✝ :: tail✝) F

State before:
D : Type
I : Interpretation D
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
V : Valuation D
M M' : MetaValuation D
F : Formula
h1 : ∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M (head✝ :: tail✝) F ↔ Holds D I V M' (head✝ :: tail✝) F
Tactic:
induction F generalizing V M M'
State after:
case cons.meta_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
a✝ : MetaVarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ (meta_var_ a✝).metaVarSet, M X V' ↔ M' X 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
a✝¹ : PredName
a✝ : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ (pred_ a✝¹ a✝).metaVarSet, M X V' ↔ M' X 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
a✝¹ a✝ : VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ (eq_ a✝¹ a✝).metaVarSet, M X V' ↔ M' X 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ true_.metaVarSet, M X V' ↔ M' X 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
a✝ : Formula
a_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ a✝.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) a✝ ↔ Holds D I V M' (head✝ :: tail✝) a✝)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ a✝.not_.metaVarSet, M X V' ↔ M' X 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ a✝¹.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) a✝¹ ↔ Holds D I V M' (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ a✝.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) a✝ ↔ Holds D I V M' (head✝ :: tail✝) a✝)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ (a✝¹.imp_ a✝).metaVarSet, M X V' ↔ M' X 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ a✝.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) a✝ ↔ Holds D I V M' (head✝ :: tail✝) a✝)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ (forall_ a✝¹ a✝).metaVarSet, M X V' ↔ M' X 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ (def_ a✝¹ a✝).metaVarSet, M X V' ↔ M' X 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
X : MetaVarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (meta_var_ X).metaVarSet, M X_1 V' ↔ M' X_1 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 Formula.metaVarSet at h1
  simp at h1
  simp only [Holds]
  exact h1 V
State after:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
X : PredName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (pred_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 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 =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
x y : VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ (eq_ x y).metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M (head✝ :: tail✝) (eq_ x y) ↔ Holds D I V M' (head✝ :: tail✝) (eq_ x y)
Tactic:
case eq_ x y =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ true_.metaVarSet, M X V' ↔ M' X 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.not_.metaVarSet, M X V' ↔ M' X 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 Formula.metaVarSet at h1
  simp only [Holds]
  congr! 1
  exact phi_ih V M M' h1
State after:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ (forall_ x phi).metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M (head✝ :: tail✝) (forall_ x phi) ↔ Holds D I V M' (head✝ :: tail✝) (forall_ x phi)
Tactic:
case forall_ x phi phi_ih =>
  unfold Formula.metaVarSet at h1
  simp only [Holds]
  apply forall_congr'
  intro a
  exact phi_ih (Function.updateITE V x a) M M' h1
State after:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
X : MetaVarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (meta_var_ X).metaVarSet, M X_1 V' ↔ M' X_1 V'
⊢ Holds D I V M (head✝ :: tail✝) (meta_var_ X) ↔ Holds D I V M' (head✝ :: tail✝) (meta_var_ X)
Tactic:
unfold Formula.metaVarSet at h1
State after:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
X : MetaVarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ {X}, M X_1 V' ↔ M' X_1 V'
⊢ 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
X : MetaVarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ {X}, M X_1 V' ↔ M' X_1 V'
⊢ Holds D I V M (head✝ :: tail✝) (meta_var_ X) ↔ Holds D I V M' (head✝ :: tail✝) (meta_var_ X)
Tactic:
simp at h1
State after:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
X : MetaVarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), M X V' ↔ M' X V'
⊢ 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
X : MetaVarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), M X V' ↔ M' X V'
⊢ Holds D I V M (head✝ :: tail✝) (meta_var_ X) ↔ Holds D I V M' (head✝ :: tail✝) (meta_var_ X)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
X : MetaVarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), M X V' ↔ M' X V'
⊢ M X V ↔ M' X V

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
X : MetaVarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), M X V' ↔ M' X V'
⊢ M X V ↔ M' X V
Tactic:
exact h1 V
State after:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
X : PredName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (pred_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
⊢ 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:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
x y : VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ (eq_ x y).metaVarSet, M X V' ↔ M' X V'
⊢ 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:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ true_.metaVarSet, M X V' ↔ M' X 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.not_.metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M (head✝ :: tail✝) phi.not_ ↔ Holds D I V M' (head✝ :: tail✝) phi.not_
Tactic:
unfold Formula.metaVarSet at h1
State after:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
⊢ 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
⊢ 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
⊢ ¬Holds D I V M (head✝ :: tail✝) phi ↔ ¬Holds D I V M' (head✝ :: tail✝) phi

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
⊢ ¬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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
⊢ 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi
Tactic:
exact phi_ih V M M' h1
State after:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ (phi.imp_ psi).metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M (head✝ :: tail✝) (phi.imp_ psi) ↔ Holds D I V M' (head✝ :: tail✝) (phi.imp_ psi)
Tactic:
unfold Formula.metaVarSet at h1
State after:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet ∪ psi.metaVarSet, M X V' ↔ M' X V'
⊢ 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet ∪ psi.metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M (head✝ :: tail✝) (phi.imp_ psi) ↔ Holds D I V M' (head✝ :: tail✝) (phi.imp_ psi)
Tactic:
simp at h1
State after:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
⊢ 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
⊢ 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
⊢ 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
⊢ 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
⊢ 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
⊢ Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi
Tactic:
apply phi_ih
State after:
case a.h.a.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
⊢ ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'

State before:
case a.h.a.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
⊢ ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
Tactic:
intro V' X a1
State after:
case a.h.a.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
V' : Valuation D
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ M X V' ↔ M' X V'

State before:
case a.h.a.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
V' : Valuation D
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ M X V' ↔ M' X V'
Tactic:
apply h1
State after:
case a.h.a.h1.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
V' : Valuation D
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet

State before:
case a.h.a.h1.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
V' : Valuation D
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet
Tactic:
left
State after:
case a.h.a.h1.a.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
V' : Valuation D
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ X ∈ phi.metaVarSet

State before:
case a.h.a.h1.a.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
V' : Valuation D
X : MetaVarName
a1 : X ∈ phi.metaVarSet
⊢ X ∈ phi.metaVarSet
Tactic:
exact a1
State after:
no goals

State before:
case a.h'.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
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:
apply psi_ih
State after:
case a.h'.a.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
a✝ : Holds D I V M' (head✝ :: tail✝) phi
⊢ ∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V'

State before:
case a.h'.a.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
a✝ : Holds D I V M' (head✝ :: tail✝) phi
⊢ ∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V'
Tactic:
intro V' X a1
State after:
case a.h'.a.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
a✝ : Holds D I V M' (head✝ :: tail✝) phi
V' : Valuation D
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ M X V' ↔ M' X V'

State before:
case a.h'.a.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
a✝ : Holds D I V M' (head✝ :: tail✝) phi
V' : Valuation D
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ M X V' ↔ M' X V'
Tactic:
apply h1
State after:
case a.h'.a.h1.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
a✝ : Holds D I V M' (head✝ :: tail✝) phi
V' : Valuation D
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet

State before:
case a.h'.a.h1.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
a✝ : Holds D I V M' (head✝ :: tail✝) phi
V' : Valuation D
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet
Tactic:
right
State after:
case a.h'.a.h1.a.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
a✝ : Holds D I V M' (head✝ :: tail✝) phi
V' : Valuation D
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ X ∈ psi.metaVarSet

State before:
case a.h'.a.h1.a.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D) (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → (M X V' ↔ M' X V')
a✝ : Holds D I V M' (head✝ :: tail✝) phi
V' : Valuation D
X : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ X ∈ psi.metaVarSet
Tactic:
exact a1
State after:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ (forall_ x phi).metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M (head✝ :: tail✝) (forall_ x phi) ↔ Holds D I V M' (head✝ :: tail✝) (forall_ x phi)
Tactic:
unfold Formula.metaVarSet at h1
State after:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
⊢ 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
⊢ 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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
⊢ (∀ (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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
⊢ (∀ (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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
⊢ ∀ (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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
⊢ ∀ (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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
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
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V'
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:
exact phi_ih (Function.updateITE V x a) M M' h1
State after:
no goals

State before:
D : Type
I : Interpretation D
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 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:
simp only [Holds]
State after:
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
⊢ (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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
⊢ (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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
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
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
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:
case pos
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
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
Tactic:
apply E_ih
State after:
case pos.h1
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ ∀ (V' : Valuation D), ∀ X ∈ E_hd.F.metaVarSet, M X V' ↔ M' X V'

State before:
case pos.h1
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ ∀ (V' : Valuation D), ∀ X ∈ E_hd.F.metaVarSet, M X V' ↔ M' X V'
Tactic:
simp only [no_meta_var_imp_meta_var_set_is_empty E_hd.F E_hd.args E_hd.nf]
State after:
case pos.h1
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ ∀ (V' : Valuation D), ∀ X ∈ ∅, M X V' ↔ M' X V'

State before:
case pos.h1
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ ∀ (V' : Valuation D), ∀ X ∈ ∅, M X V' ↔ M' X V'
Tactic:
simp
State after:
no goals

State before:
case neg
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
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)
Tactic:
apply E_ih
State after:
case neg.h1
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'

State before:
case neg.h1
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
Tactic:
unfold Formula.metaVarSet
State after:
case neg.h1
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ ∀ (V' : Valuation D), ∀ X ∈ ∅, M X V' ↔ M' X V'

State before:
case neg.h1
D : Type
I : Interpretation D
E_hd : Definition
E_tl : List Definition
E_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M E_tl F ↔ Holds D I V M' E_tl F)
X : DefName
xs : List VarName
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X_1 ∈ (def_ X xs).metaVarSet, M X_1 V' ↔ M' X_1 V'
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ ∀ (V' : Valuation D), ∀ X ∈ ∅, M X V' ↔ M' X V'
Tactic:
simp
State after:
no goals