proposition: Lemma CompileCallFacadeImplementationWW: forall {av} {env} fWW, forall fpointer varg (arg: W) tenv, GLabelMap.MapsTo fpointer (Axiomatic (FacadeImplementationWW av fWW)) env -> forall vret ext, vret ∉ ext -> NotInTelescope vret tenv -> StringMap.MapsTo varg (wrap arg) ext -> {{ tenv }} Call vret fpointer (varg :: nil) {{ [[ `vret ->> (fWW arg) as _]]:: tenv }} ∪ {{ ext }} // env.
proof: Proof. repeat match goal with | _ => SameValues_Facade_t_step | _ => facade_cleanup_call end; facade_eauto. Qed.
imports: CertifiedExtraction.Extraction.External.Core CertifiedExtraction.Extraction.External.GenericMethods Coq.Lists.List