proposition: Lemma implies_in_combine : forall A B (l1 : list A) (l2 : list B) x, length l1 = length l2 -> LIn x l1 -> {y : B $ LIn (x, y) (combine l1 l2)}.
proof: Proof. induction l1; simpl; sp; destruct l2; allsimpl; subst; sp; invertsn H. exists b; sp. apply IHl1 with(x:=x) in H; sp. exists y; sp. Qed.
imports: UsefulTypes bin_rels Omega