proposition: Lemma CompileCallEmpty: forall `{FacadeWrapper (Value av) A} `{FacadeWrapper av (list A)} (vtest vlst : StringMap.key) (env : GLabelMap.t (FuncSpec av)) (tenv: Telescope av) ext (fempty : GLabelMap.key) (lst : list A), vlst <> vtest -> vtest ∉ ext -> Lifted_MapsTo ext tenv vlst (wrap lst) -> Lifted_not_mapsto_adt ext tenv vtest -> GLabelMap.MapsTo fempty (Axiomatic (List_empty _)) env -> {{ tenv }} Call vtest fempty (vlst :: nil) {{ [[`vtest ->> (bool2w match lst with | nil => true | _ :: _ => false end) as _]]::(DropName vtest tenv) }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t); [ facade_eauto.. | ]. rewrite <- remove_add_comm by congruence. apply DropName_remove. eauto. rewrite <- add_redundant_cancel; eauto. Qed.
imports: CertifiedExtraction.Extraction.External.Core