proposition: Lemma in_combine : forall A B a b, forall l1 : list A, forall l2 : list B, LIn (a,b) (combine l1 l2) -> LIn a l1 # LIn b l2.
proof: Proof. induction l1; introv Hlin; simpl; sp; destruct l2; allsimpl; sp; allapply pair_inj; repnd; subst; sp; apply_in_hyp p; sp. Qed.
imports: UsefulTypes bin_rels Omega