proposition: Lemma combine_in_right : forall T1 T2 (l2: list T2) (l1: list T1), (length l2 <= length l1) -> forall u2, ( LIn u2 l2) -> {u1 : T1 $ LIn (u1,u2) (combine l1 l2)}.
proof: Proof. induction l2; intros ? Hlen ? Hin. inverts Hin as Hin; simpl in Hlen. destruct l1 ; simpl in Hlen. omega. inverts Hin as Hin. - subst. exists t. simpl. left; auto. - apply IHl2 with l1 u2 in Hin; auto. parallel u Hcom. simpl. right; auto. omega. Qed.
imports: UsefulTypes bin_rels Omega