proposition: Lemma CompileCallFacadeImplementationOfCopy: forall `{FacadeWrapper av A} {env}, forall fpointer vsrc, GLabelMap.MapsTo fpointer (Axiomatic (FacadeImplementationOfCopy A)) env -> forall vret (adt: A) (ext: StringMap.t (Value av)) (tenv: Telescope av), vret <> vsrc -> vret ∉ ext -> NotInTelescope vret tenv -> StringMap.MapsTo vsrc (wrap adt) ext -> {{ tenv }} (Call vret fpointer (vsrc :: nil)) {{ [[ `vret ->> adt as _]] :: tenv }} ∪ {{ ext }} // env.
proof: Proof. repeat match goal with | _ => SameValues_Facade_t_step | _ => facade_cleanup_call end. facade_eauto. facade_eauto. facade_eauto. Qed.
imports: Coq.Lists.List CertifiedExtraction.Extraction.External.Core