proposition: Lemma list_pred_app_both : forall (A B : Set)(P : A -> B -> Prop)(lsa1 lsa2 : list A)(lsb1 lsb2 : list B), list_pred P lsa1 lsb1 -> list_pred P lsa2 lsb2 -> list_pred P (lsa1 ++ lsa2) (lsb1 ++ lsb2).
proof: Proof. induction lsa1; destruct lsb1; intuition. inversion H. inversion H. inversion H; clear H; subst. repeat rewrite <- app_comm_cons. econstructor. trivial. eauto. Qed.
imports: FCF.FCF Permutation