simp only [admits] at h1
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admits τ F
⊢ admitsAux τ ∅ F
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
F : Formula
h1 : admitsAux τ ∅ F
⊢ admitsAux τ ∅ F