cases h1
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList vs phi ∧ NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v phi ∧ NotFree Γ v psi
case intro
v : VarName
Γ : List (VarName × MetaVarName)
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → v ∉ vs → NotFree Γ v psi
vs : List VarName
h2 : v ∉ vs
left✝ : NoMetaVarAndAllFreeInList vs phi
right✝ : NoMetaVarAndAllFreeInList vs psi
⊢ NotFree Γ v phi ∧ NotFree Γ v psi