proposition: Theorem pred_firstn_In : forall (A : Set) ls1 ls2, list_pred (fun x0 y : list A => exists n : nat, y = firstn n x0) ls1 ls2 -> forall a, In a (flatten ls2) -> In a (flatten ls1).
proof: Proof. induction 1; intuition; simpl in *. destruct H. subst. eapply in_app_or in H1. intuition. eapply in_or_app. left. eapply firstn_In. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation