proposition: Theorem In_combine_NoDup_eq_r : forall (A B : Set)(lsa : list A)(lsb : list B) a b1 b2, NoDup lsa -> In (a, b1) (combine lsa lsb) -> In (a, b2) (combine lsa lsb) -> b1 = b2.
proof: Proof. induction lsa; intuition; simpl in *. intuition. destruct lsb. simpl in *. intuition. inversion H; clear H; subst. simpl in *. intuition. repeat pairInv. trivial. pairInv. eapply in_combine_l in H0. intuition. pairInv. eapply in_combine_l in H. intuition. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation