The main lemma in this file, concretize?_wfl_some, proves that εnv.concretize? x succeeds when εnv is a literal symbolic environment that is well-formed with respect to x.

@[irreducible]

theorem Cedar.Thm.wf_term_implies_valid_uids {t : SymCC.Term} {εs : SymCC.SymEntities} : SymCC.Term.WellFormed εs t → ∀ (uid : Spec.EntityUID), uid ∈ t.entityUIDs → εs.isValidEntityUID uid = true

theorem Cedar.Thm.concretize?_wfl_implies_some {x : Spec.Expr} {εnv : SymCC.SymEnv} : εnv.WellFormedLiteralFor x → ∃ (env : Spec.Env), SymCC.SymEnv.concretize? x εnv = some env