proposition: Lemma combine_app : forall r1 r2 s1 s2, length r1 = length s1 -> combine (r1++r2) (s1++s2) = (combine r1 s1)++(combine r2 s2).
proof: Proof. Proof using. intros r1. induction r1; introv E; destruct s1; tryfalse. { auto. } { rew_list in *. do 2 rewrite combine_cons. rew_list. rewrite~ IHr1. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)