given expression should not contain de-Bruijn variables

Stream: new members

[Lucas Allen]

G'day. I have the following meta code

meta def recurse_pi : expr → tactic unit
| (expr.pi _ _ v b) := do t ← infer_type v,
                          trace t,
                          recurse_pi b
| _ := skip

#eval recurse_pi `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))

I want this to print out

Type
Type
Prop
Prop

But it prints out

Type
Type

and gives the error "tactic 'infer_type' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic"

How do I replace de-Bruijn variables with local constants? And/or is there a better way to do what I want? Thanks.