It seems to me that if, in the third step of my proof, I could convert the *left (pure fst)* into *left (first <?>)*, then I could use the **distribution** axiom to convert *pure distr >>> left (first <?>)* into *first (left <?>) >>> pure distr *. At that point, I would have (starting from the left side of my expression): *first (..) >>> first (..)*, and could apply the functor property of *first*, in order to simplify the expression.