proposition: Lemma list_pred_symm : forall (A B : Set)(P : A -> B -> Prop) lsa lsb, list_pred (fun b a => P a b) lsb lsa -> list_pred P lsa lsb.
proof: Proof. induction lsa; inversion 1; intuition; simpl in *; econstructor. subst. trivial. subst. trivial. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation