proposition: Theorem list_pred_rev : forall (A B : Set)(lsa : list A)(lsb : list B) P, list_pred P lsa lsb -> forall a b, P a b -> list_pred P (lsa ++ (a :: nil)) (lsb ++ (b :: nil)).
proof: Proof. induction 1; intuition. repeat rewrite app_nil_l. econstructor. intuition. econstructor. repeat rewrite <- app_comm_cons. econstructor; intuition. Qed.
imports: FCF.FCF Permutation