proposition: Theorem In_zip_strong : forall (A B : Set)(ls : list A) f a (b : B), In (a, b) (zip ls (map f ls)) -> (In a ls /\ b = f a).
proof: Proof. induction ls; intuition; simpl in *. intuition. intuition. pairInv. intuition. right. eapply IHls. eauto. intuition. pairInv. trivial. eapply IHls; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation