proposition: Lemma CompileRead: forall {av} name var (val: W) ext (tenv: Telescope av), name ∉ ext -> NotInTelescope name tenv -> StringMap.MapsTo var (wrap val) ext -> forall env, {{ tenv }} (Assign name (Var var)) {{ [[`name ->> val as _]]::tenv }} ∪ {{ ext }} // env.
proof: Proof. SameValues_Facade_t. Qed.
imports: CertifiedExtraction.StringMapUtils CertifiedExtraction.ExtendedLemmas CertifiedExtraction.TelAppend