Help trying to prove that something is inside a Map.

Stream: new members

[Felipe GS]

I'm trying to prove that some thing is inside a map. But I'm having problems with the pattern matching of Prop...

inductive MapImpl : Type u → Type v → Type (max u v + 1)
    | empty : MapImpl α β
    | node  : MapImpl α β → α → β → MapImpl α β → MapImpl α β
    deriving Repr

 inductive MapImpl.Member [LT α]: α → (MapImpl α β) -> Prop
    | here    : Member k (MapImpl.node l k v r)
    | inLeft  : Member k l → (k < c) → Member k (MapImpl.node l c v r)
    | inRight : Member k r → (k > c) → Member k (MapImpl.node l c v r)

def MapImpl.find [DecidableEq α] [LT α] [DecidableRel (@LT.lt α _)] [Ord α] : (s: MapImpl α β) → (k: α) → MapImpl.Member k s → β
    | MapImpl.empty,        key, proof => nomatch proof
    | MapImpl.node l k v r, key, proof =>
      match (decEq k key) with
      | Decidable.isTrue  _ => v
      | Decidable.isFalse _ =>
          dite (LT.lt key k) sorry sorry