proposition: Lemma CompileCallFacadeImplementationOfMutation_ADT: forall {av Targ Tadt} `{FacadeWrapper av Tadt} `{FacadeWrapper av Targ} (env : GLabelMap.t (FuncSpec av)) (fADT : Targ -> Tadt -> Tadt) (fpointer : GLabelMap.key) (varg vtmp : StringMap.key) (arg : Targ) (target : Tadt) (tenv : Telescope av), GLabelMap.MapsTo fpointer (Axiomatic (FacadeImplementationOfMutation_ADT Targ Tadt fADT)) env -> forall (vret : StringMap.key) (ext : StringMap.t (Value av)), PreconditionSet tenv ext [[[varg; vtmp; vret]]] -> {{ [[`vret ->> target as _]]::[[`varg ->> arg as _]]::tenv }} Call vtmp fpointer (vret :: varg :: nil) {{ [[`vret ->> fADT arg target as _]]::tenv }} ∪ {{ ext }} // env.
proof: Proof. repeat match goal with | _ => SameValues_Facade_t_step | _ => facade_cleanup_call | _ => PreconditionSet_t end. facade_eauto. facade_eauto. rewrite remove_remove_comm by congruence. facade_eauto. Qed.
imports: Coq.Lists.List CertifiedExtraction.Extraction.External.Core