proposition: Lemma list_pred_single : forall (A : Set) (P : A -> A -> Prop) (lsa : list A), (forall a, In a lsa -> P a a) -> list_pred P lsa lsa.
proof: Proof. induction lsa; intuition; simpl in *; econstructor. eapply H. intuition. eauto. Qed.
imports: FCF.FCF Permutation