proposition: Lemma unshift_app : forall s t, unshift (s ++ t) = unshift s ++ unshift t.
proof: Proof. induction s; cbn. - reflexivity. - intro; destruct a; auto. now rewrite (IHs t). Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)