I’m having a plumbing issue. I’ve got the following code — mostly irrelevant, only the last six lines matter:

-- monoids presented as an associative binary operation
record Monoid2 (A : Set) : Set where
  constructor mkMonoid2
  field
    bop : (A -> A -> A)
    id : A
    l_ident : ∀ {a} -> bop id a ≡ a
    r_ident : ∀ {a} -> bop a id ≡ a
    assoc : ∀ {a b c} -> bop (bop a b) c ≡ bop a (bop b c)

-- monoids presented as an associative n-ary operation
record MonoidN (A : Set) : Set where
  constructor mkMonoidN
  field
    op : List A -> A
    opPure≡id : ∀ {a} -> op (a ∷ []) ≡ a
    opMapOp≡opFlattened : ∀ {ll : List (List A)} -> op (Data.List.map op ll) ≡ op (Data.List.concat ll)

monoid2toN : ∀ {A} -> Monoid2 A -> MonoidN A
monoid2toN {A} (mkMonoid2 bop id l_ident r_ident assoc) = mkMonoidN op l_ident (λ {ll} -> induction ll) where
  op : List A -> A
  op as = Data.List.foldl bop id as
  lemma : bop id (op []) ≡ id
  lemma = l_ident
  induction : (ll : List (List A)) -> op (Data.List.map op ll) ≡ op (Data.List.concat ll)
  induction [] = refl
  induction ([] ∷ ll) = {! refl !}
  induction ((x ∷ l) ∷ ll) = {!!}

When I try to give the goal {! refl !} to agda, it complains:

bop id (op []) != id of type A
when checking that the expression refl has type
op (Data.List.map op ([] ∷ ll)) ≡ op (Data.List.concat ([] ∷ ll))

However, you may notice that I do have a proof of said equality, named “lemma”. I am just not sure how to plug it in properly so agda knows to use it.