internlm/Lean-Github huggingface dataset:
Theorem: MM0.holds_coincide_meta_var
Proof 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
Proof state after:
no goals
Theorem: MM0.holds_coincide_meta_var
Proof 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]
Proof state after:
no goals
Theorem: MM0.holds_coincide_meta_var
Proof 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]
Proof state after:
no goals
Theorem: MM0.holds_coincide_meta_var
Proof 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]
Proof state after:
no goals
Theorem: MM0.holds_coincide_meta_var
Proof 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
Proof 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_
Theorem: MM0.holds_coincide_meta_var
Proof 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]
Proof 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
Theorem: MM0.holds_coincide_meta_var
Proof 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
Proof 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
Theorem: MM0.holds_coincide_meta_var
Proof 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
Proof state after:
no goals
Theorem: MM0.holds_coincide_meta_var
Proof 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
Proof 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)
Theorem: MM0.holds_coincide_meta_var
Proof 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
Proof 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)
Theorem: MM0.holds_coincide_meta_var
Proof 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]
Proof 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
Theorem: MM0.holds_coincide_meta_var
Proof 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
Proof 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
Theorem: MM0.holds_coincide_meta_var
Proof 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
Proof 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'
Theorem: MM0.holds_coincide_meta_var
Proof 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
Proof 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'
Theorem: MM0.holds_coincide_meta_var
Proof 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
Proof 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
Theorem: MM0.holds_coincide_meta_var
Proof 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
Proof 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