proposition: Lemma CompileCallPop: forall `{FacadeWrapper (Value av) A} `{FacadeWrapper av (list A)} (vhead vlst : StringMap.key) (env : GLabelMap.t (FuncSpec av)) tenv ext (fpop : GLabelMap.key) head (tail : list A), vlst <> vhead -> vhead ∉ ext -> vlst ∉ ext -> Lifted_MapsTo ext tenv vlst (wrap (head :: tail)) -> Lifted_not_mapsto_adt ext tenv vhead -> GLabelMap.MapsTo fpop (Axiomatic (List_pop _)) env -> {{ tenv }} Call vhead fpop (vlst :: nil) {{ [[`vhead ->> head as _]]::[[`vlst ->> tail as _]]::(DropName vlst (DropName vhead tenv)) }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t); facade_eauto. Qed.
imports: CertifiedExtraction.Extraction.External.Core