filter_distributes_over_append

Feb 5 at 1:09 AM
Dafny beginner here, and I'm struggling with what I assume is a simple proof.

If I define a sequence filtering function as follows:
    function method filter<T>(xs: seq<T>, pred: T -> bool): seq<T>
        reads pred.reads
        requires forall t :: pred.requires(t)
        ensures forall x :: x in xs && pred(x) ==> x in filter(xs, pred)
        ensures forall x :: x in filter(xs, pred) ==> x in xs && pred(x)
    {
        if |xs| == 0 then []
        else if pred(xs[0]) then [xs[0]] + filter(xs[1..], pred)
        else filter(xs[1..], pred)
    }
How might I prove that this function distributes over an append?
    lemma filter_distributes_over_append<T>(xs1: seq<T>, xs2: seq<T>, pred: T -> bool)
        requires forall t :: pred.requires(t)
        ensures filter(xs1 + xs2, pred) == filter(xs1, pred) + filter(xs2, pred)
Any tips and techniques would be much appreciated! Thanks!
Feb 5 at 1:47 AM
Had a flash of insight and came up with the following, but to be honest, it feels a bit like write-only code. Any suggestions for making this proof clearer?
    lemma append_associative<T>(xs: seq<T>, ys: seq<T>, zs: seq<T>)
        ensures (xs + ys) + zs == xs + (ys + zs)
    {}

    lemma filter_distributes_over_append<T>(xs1: seq<T>, xs2: seq<T>, pred: T -> bool)
        requires forall t :: pred.requires(t)
        ensures filter(xs1 + xs2, pred) == filter(xs1, pred) + filter(xs2, pred)
    {
        if (xs1 == []) {
        } else if pred(xs1[0]) {
            calc == {
                filter(xs1 + xs2, pred); { assert xs1 == [xs1[0]] + xs1[1..]; }
                filter(([xs1[0]] + xs1[1..]) + xs2, pred); { append_associative([xs1[0]], xs1[1..], xs2); }
                filter([xs1[0]] + (xs1[1..] + xs2), pred);
                [xs1[0]] + filter(xs1[1..] + xs2, pred);
                [xs1[0]] + filter(xs1[1..], pred) + filter(xs2, pred);
                filter([xs1[0]], pred) + filter(xs1[1..], pred) + filter(xs2, pred);
                filter([xs1[0]] + xs1[1..], pred) + filter(xs2, pred);
                filter(xs1, pred) + filter(xs2, pred);
            }
        } else {
            calc == {
                filter(xs1 + xs2, pred); { assert xs1 == [xs1[0]] + xs1[1..]; }
                filter(([xs1[0]] + xs1[1..]) + xs2, pred); { append_associative([xs1[0]], xs1[1..], xs2); }
                filter([xs1[0]] + (xs1[1..] + xs2), pred);
                [] + filter(xs1[1..] + xs2, pred);
                filter(xs1[1..] + xs2, pred);
                filter(xs1, pred) + filter(xs2, pred);
            }
        }
    }