proposition: Lemma combine_in_left : 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; inversion Hlen. - subst. exists t. simpl. left; auto. - apply IHl1 with l2 u1 in Hin; auto. parallel u2 Hcom. simpl. right; auto. Qed.
imports: UsefulTypes bin_rels Omega