Distributivity of Sequence Map over Function Composition in Dafny lemma MapDistributivity(xs:seq, f:int->int, g:int->int) requires forall x :: x in xs ==> f.requires(x); requires forall x …