proposition: Lemma CompileConstantBool: forall {av} name env (b: bool) ext (tenv: Telescope av), name ∉ ext -> NotInTelescope name tenv -> {{ tenv }} (Assign name (Const (bool2w b))) {{ [[`name ->> b as _]]::tenv }} ∪ {{ ext }} // env.
proof: Proof. SameValues_Facade_t. change (wrap (bool2w b)) with (wrap (FacadeWrapper := (@FacadeWrapper_bool av)) b). SameValues_Facade_t. Qed.
imports: CertifiedExtraction.StringMapUtils CertifiedExtraction.ExtendedLemmas CertifiedExtraction.TelAppend