This file contains the completeness theorems of Sym.ofEnv

theorem Cedar.Thm.ofEnv_completeness {Γ : Validation.TypeEnv} {env : Spec.Env} (hwf_Γ : Γ.WellFormed) (hwf_env : env.StronglyWellFormed) (henum_comp : SymCC.Env.EnumCompleteFor env (SymCC.SymEnv.ofEnv Γ)) (hinst : env∈ᵢSymCC.SymEnv.ofEnv Γ) : InstanceOfWellFormedEnvironment env.request env.entities Γ