Theorem: MM0.holds_coincide_meta_var_no_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 : F.metaVarSet = ∅
⊢ Holds D I V M E F ↔ Holds D I V M' E F
Tactic:
apply holds_coincide_meta_var
State after:
case h1
D : Type
I : Interpretation D
V : Valuation D
M M' : MetaValuation D
E : Env
F : Formula
h1 : F.metaVarSet = ∅
⊢ ∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V'

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

State before:
case h1
D : Type
I : Interpretation D
V : Valuation D
M M' : MetaValuation D
E : Env
F : Formula
h1 : F.metaVarSet = ∅
⊢ ∀ (V' : Valuation D), ∀ X ∈ ∅, M X V' ↔ M' X V'
Tactic:
simp
State after:
no goals