unfold NotFree at h1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
psi_ih : NotFree Γ v psi → IsNotFree D I M E psi v
h1 : NotFree Γ v (phi.imp_ psi)
⊢ IsNotFree D I M E (phi.imp_ psi) v
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
phi psi : Formula
phi_ih : NotFree Γ v phi → IsNotFree D I M E phi v
psi_ih : NotFree Γ v psi → IsNotFree D I M E psi v
h1 : NotFree Γ v phi ∧ NotFree Γ v psi
⊢ IsNotFree D I M E (phi.imp_ psi) v