proposition: Lemma list_pred_impl : forall (A B : Set)(lsa : list A)(lsb : list B) (P1 : A -> B -> Prop), list_pred P1 lsa lsb -> forall (P2 : A -> B -> Prop), (forall a b, P1 a b -> P2 a b) -> list_pred P2 lsa lsb.
proof: Proof. induction 1; intuition; simpl in *. econstructor. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation