FreeAddSemigroup.instMonad =
  { map := fun {α β} f x => (fun {α β} x f => (FreeAddSemigroup.lift f) x) x ((fun {α} => FreeAddSemigroup.of) ∘ f),
    pure := fun {α} => FreeAddSemigroup.of,
    seq := fun {α β} f x =>
      (fun {α β} x f => (FreeAddSemigroup.lift f) x) f fun y =>
        (fun {α β} x f => (FreeAddSemigroup.lift f) x) (x ()) ((fun {α} => FreeAddSemigroup.of) ∘ y),
    seqLeft := fun {α β} x y =>
      (fun {α β} x f => (FreeAddSemigroup.lift f) x) x fun a =>
        (fun {α β} x f => (FreeAddSemigroup.lift f) x) (y ()) fun x => (fun {α} => FreeAddSemigroup.of) a,
    seqRight := fun {α β} x y => (fun {α β} x f => (FreeAddSemigroup.lift f) x) x fun x => y (),
    bind := fun {α β} x f => (FreeAddSemigroup.lift f) x }