{A B C : Type} (f : A -> B -> C) (def_l : list A -> list C) (def_r : list B -> list C) l1 l2 := match l1, l2 with | nil, nil => nil | nil, _ => def_r l2 | _, nil => def_l l1 | x :: l1, y :: l2 => (f x y) :: ( f def_l def_r l1 l2) end.
Require Import Basics.Overture.