proposition: Lemma length_combine : forall r s, length r = length s -> length (combine r s) = length r.
proof: Proof. Proof using. intros r. induction r; introv E; destruct s; tryfalse. { auto. } { rewrite combine_cons. rew_list~. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)