proposition: Lemma split_length : forall l r s, (r,s) = split l -> length r = length l /\ length s = length l.
proof: Proof. Proof using. intros l. induction l as [|[x y] l']; introv E. { rewrite split_nil in E. inverts~ E. } { rewrite split_cons_let in E. destruct (split l') as [r' s']. inverts E. rew_list. forwards~ (?&?): IHl'. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)