proposition: Lemma length_combine_eq : forall {A B: Type} (la:list A) (lb: list B), length la =length lb -> length (combine la lb) = length la.
proof: Proof. introv XX. rewrite combine_length. rewrite XX. apply Min.min_idempotent. Qed.
imports: UsefulTypes bin_rels Omega