proposition: Lemma CompileConstant_SCA: forall {A} {Wr: FacadeWrapper W A} name env (w: A) ext (tenv: Telescope _), name ∉ ext -> NotInTelescope name tenv -> {{ tenv }} (Assign name (Const (wrap w))) {{ [[`name ->> w as _]]::tenv }} ∪ {{ ext }} // env.
proof: Proof. intros. rewrite (TelEq_same_wrap w (wrap (FacadeWrapper := Wr) w)) by reflexivity. auto using CompileConstant. Qed.
imports: Fiat.CertifiedExtraction.Extraction.Extraction Fiat.CertifiedExtraction.Extraction.BinEncoders.Basics Fiat.CertifiedExtraction.Extraction.BinEncoders.Wrappers Fiat.CertifiedExtraction.Extraction.BinEncoders.Properties Coq.Program.Program Coq.Lists.List