fact: Definition remove_from {X} : list X -> list (X * list X) := let fix remove_from_ pre xs := match xs with | [] => [] | x :: xs' => (x, pre ++ xs') :: remove_from_ (pre ++ [x]) xs' end in remove_from_ [].
imports: Coq(List) ITree(Basics.Basics Core.ITreeDefinition Indexed.Sum Core.Subevent Events.Exception)