proposition: Lemma CompileCallFacadeImplementationOfMutation_SCA: forall `{H : FacadeWrapper av A} (env : GLabelMap.t (FuncSpec av)) (fADT : W -> A -> A) (fpointer : GLabelMap.key) (varg vtmp : StringMap.key) (arg : W) (target : A) (tenv : Telescope av), GLabelMap.MapsTo fpointer (Axiomatic (FacadeImplementationOfMutation_SCA _ 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 (SameValues_Facade_t_step || facade_cleanup_call || PreconditionSet_t); facade_eauto. Qed.
imports: Coq.Lists.List CertifiedExtraction.Extraction.External.Core