proposition: Lemma split_app : forall l1 l2 r1 r2 s1 s2, (r1,s1) = split l1 -> (r2,s2) = split l2 -> split (l1++l2) = (r1++r2, s1++s2).
proof: Proof. Proof using. intros l1. induction l1 as [|[x y] l1']; introv H1 H2. { rewrite split_nil in H1. inverts~ H1. } { rewrite split_cons_let in H1. destruct (split l1') as [r1' s1']. inverts H1. rew_list. rewrite split_cons_let. erewrite~ (IHl1' l2). } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)