The main lemma in this file, concretize?_some_wf, proves that εnv.concretize? x produces an environment that is well-formed for x.

theorem Cedar.Thm.concretize?_some_wf {x : Spec.Expr} {env : Spec.Env} {εnv : SymCC.SymEnv} : εnv.WellFormedFor x → SymCC.SymEnv.concretize? x εnv = some env → env.WellFormedFor x