proposition: Theorem list_pred_app_both_if : forall (A B : Set) P (x y : list A)(z q : list B), length x = length z -> list_pred P (x ++ y) (z ++ q) -> list_pred P x z /\ list_pred P y q.
proof: Proof. intros. eapply list_pred_app in H0. rewrite H in H0. rewrite ?firstn_app, ?skipn_app, ?firstn_ge_all, ?Nat.sub_diag, ?firstn_O, ?app_nil_r in * by lia. firstorder. Qed.
imports: FCF.FCF Permutation