proposition: Lemma filter_app_inv {A} : forall pred (l l1 l2 : list A), filter pred l = app l1 l2 -> exists l1' l2', l = app l1' l2' /\ l1 = filter pred l1' /\ l2 = filter pred l2'.
proof: Proof. induction l; simpl; intros. - destruct l1; simpl in *; [ destruct l2; [ eexists nil; eexists nil; intuition | discriminate] | discriminate ]. - revert H; case_eq (pred a); intros. + destruct l1; simpl in *. * destruct l2; [ discriminate | ]. injection H0; intros. apply (IHl [] l2) in H1; destruct_ex; intuition; subst. eexists []; eexists (_ :: _); intuition; simpl. rewrite H, H0; reflexivity. * injection H0; intros. apply IHl in H1; destruct_ex; subst. eexists (a0 :: x); eexists x0; intuition. rewrite H2; reflexivity. simpl; rewrite H, H1; reflexivity. + apply IHl in H0; destruct_ex; subst. eexists (a :: x); eexists x0; intuition. rewrite H1; reflexivity. simpl; rewrite H, H0; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts