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