proposition: Lemma in_combine_right_eauto : forall (A B : Type) a b, forall l1 : list A, forall l2 : list B, LIn (a,b) (combine l1 l2) -> LIn b l2.
proof: Proof. introv Hin. apply in_combine in Hin; spc. Qed.
imports: UsefulTypes bin_rels Omega