resetting instance cache in term mode?

Stream: new members

[Matt Diamond]

Is there a way to reset the instance cache when writing definitions in term mode? I'm wondering if there's a cleaner way to write this:

def comp_dec {α : Type*} {p : α → Prop} (d : decidable_pred p) (f : α → α) : decidable_pred (p ∘ f) :=
λ a, dite (p (f a)) is_true is_false

def ε : Π (n : ℕ) (p : cantor → Prop) [decidable_pred p], cantor
| 0 _ _         := λ _, zero
| (n+1) p p_dec :=
  let p_zero := p ∘ cons zero,
      p_one := p ∘ cons one,
      p_zero_dec := comp_dec p_dec (cons zero),
      p_one_dec := comp_dec p_dec (cons one),
      ite_prop_dec := p_zero_dec (@ε n p_zero ‹_›) in
  @ite _ (p_zero (@ε n p_zero ‹_›)) ‹_›
    (zero :: @ε n p_zero ‹_›)
    (one :: @ε n p_one ‹_›)

(The type cantor is an alias for stream bit, where bit is an enumerated type with values of zero or one.)

This function performs a limited search of the Cantor space, and you can see that it involves a lot of passing around decidable and decidable_pred instances. I'm wondering if there's a way to avoid that... like an equvalent of resetI but for term mode. This would allow me to get rid of comp_dec, which I think is only necessary because Lean doesn't know that the function being composed is decidable.