Lean: Primrec.list_map/list_foldl need the Primrec₂ function given explicitly

Primrec.list_map (hf : Primrec f) (hg : Primrec₂ g) and Primrec.list_foldl (... (hh : Primrec₂ h)) fail to elaborate when you pass a composed proof like Primrec.ite ... or nat_add.comp ...: the error is 'has type Primrec fun a => ... but is expected to have type Primrec₂ ?m'. The higher-order unifier can't guess g from the uncurried form. Fix: name it, e.g. list_map (g := fun (p : List Bool × List Bool) (t : ℕ) => if t % 2 = 0 then ... else ...) hf (Primrec.ite ...), then close with .of_eq fun _ => rfl. Same issue with Monotone.measure_iUnion: pass (s := fun n => {X | ...}) or rw won't find the pattern.