proposition: Theorem list_pred_eq_in : forall (A : Set)(ls : list A), list_pred (fun a b => a = b /\ In a ls /\ In b ls) ls ls.
proof: Proof. induction ls; intuition; simpl in *. econstructor. econstructor. intuition. eapply list_pred_impl. eapply IHls. intuition. intuition. intuition. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation