proposition: Lemma list_pred_flatten_both : forall (A B : Set)(P : A -> B -> Prop)(lsa : list (list A))(lsb : list (list B)), list_pred (list_pred P) lsa lsb -> list_pred P (flatten lsa) (flatten lsb).
proof: Proof. induction 1; intuition; simpl in *. econstructor. eapply list_pred_app_both; intuition. Qed.
imports: FCF.FCF Permutation