proposition: Lemma fusion_eq3 : forall (n : nat) (ns : list nat) (m : nat) (ms : list nat), fusion (Cons nat n ns) (Cons nat m ms) = si (list nat) (inf_egal n m) (Cons nat n (fusion ns (Cons nat m ms))) (Cons nat m (fusion (Cons nat n ns) ms)).
proof: Proof. auto. Qed.