MakeLemma doesn't transport erasable implicit arguments that must be explicitly bound for type checking

[stephen-smith]

Steps to Reproduce

data BNat = BZ | O BNat | E BNat

bnat_ind : {0 p : BNat -> Type}
        -> p BZ
        -> ((bn : BNat) -> p bn -> p (O bn))
        -> ((bn : BNat) -> p bn -> p (E bn))
        -> (bn : BNat) -> p bn
bnat_ind pbz po pe = go
 where
  go : (bn : BNat) -> p bn
  go BZ = ?pbz_hole
  go (O x) = po x (go x)
  go (E x) = pe x (go x)

Use MakeLemma <LocalLeader>l (in vim) on the ?pbz_hole in the above

Expected Behavior

Lemma would be created that would type-check, but would have no body; hole would be replaced with call to lemma OR lemma creation would fail completely.

Observed Behavior

Lemma is created:

pbz_hole : ((bn : BNat) -> p bn -> p (E bn)) -> ((bn : BNat) -> p bn -> p (O bn)) -> p BZ -> p BZ

But, that doesn't type check:

file:loc:While processing type of pbz_hole at talia.idr:16:1--18:1:                                                                              
Undefined name p

(and then further failures since pbz_hole ends up not bound in the global context.)

(Migrated from edwinb/idris2-vim#3)