proposition: Lemma filter_commute : forall {A} f g seq, @filter A f (filter g seq) = filter g (filter f seq).
proof: Proof. induction seq; simpl; intros; trivial. destruct (f a) eqn:eqf; destruct (g a) eqn:eqg; simpl; rewrite ?eqf, ?eqg, ?IHseq; trivial. 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