fact: Definition max_prefix : list A → list A → list A * list A * list A := fix go l1 l2 := match l1, l2 with | [], l2 => ([], l2, []) | l1, [] => (l1, [], []) | x1 :: l1, x2 :: l2 => if decide_rel (=) x1 x2 then prod_map id (x1 ::.) (go l1 l2) else (x1 :: l1, x2 :: l2, []) end.
imports: stdpp(options)