fact: Fixpoint fusion (x : list nat) : list nat -> list nat := fun y : list nat => match x with | Nil => y | Cons n l0 => (fix fusion_r (y : list nat) : list nat := match y with | Nil => x | Cons n0 l2 => si (list nat) (inf_egal n n0) (Cons nat n (fusion l0 (Cons nat n0 l2))) (Cons nat n0 (fusion_r l2)) end) y end.