proposition: Lemma CompileConstant: forall {av} name env w ext (tenv: Telescope av), name ∉ ext -> NotInTelescope name tenv -> {{ tenv }} (Assign name (Const w)) {{ [[`name ->> w as _]]::tenv }} ∪ {{ ext }} // env.
proof: Proof. SameValues_Facade_t. Qed.
imports: CertifiedExtraction.StringMapUtils CertifiedExtraction.ExtendedLemmas CertifiedExtraction.TelAppend