proposition: Lemma CompileWordList_pop: forall (vhead vlst : StringMap.key) (env : GLabelMap.t (FuncSpec QsADTs.ADTValue)) tenv ext (fpop : GLabelMap.key) head (tail : list W), vlst <> vhead -> vhead ∉ ext -> vlst ∉ ext -> Lifted_MapsTo ext tenv vlst (wrap (FacadeWrapper := WrapInstance (H := QS_WrapWordList)) (head :: tail)) -> Lifted_not_mapsto_adt ext tenv vhead -> GLabelMap.MapsTo fpop (Axiomatic QsADTs.WordListADTSpec.Pop) env -> {{ tenv }} Call vhead fpop (vlst :: nil) {{ [[`vhead ->> head as _]]::[[(NTSome vlst (H := WrapInstance (H := QS_WrapWordList))) ->> 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.QueryStructures.CallRules.Core