proposition: Lemma combine_app_eq: forall A B (l1:list A) (l21 l22: list B), length l1 <= length l21 -> combine l1 l21 = combine l1 (l21 ++ l22).
proof: Proof. induction l1; intros ? ? Hle; simpl; auto. destruct l21; simpl. inverts Hle. rewrite <- IHl1; allsimpl; try omega; auto. Qed.
imports: UsefulTypes bin_rels Omega