implicit assumptions in functions

Stream: new members

[Simon Daniel]

Hello
I Have the following Option like inductive, signifiing the existance of an value for an String

inductive W (a: Type) (s: String) where
| Wrap: a -> W a s
| Empty: W a s

def wrap {a} (v:a) (s: String): W a s:=
  .Wrap v

def is_empty: W a l -> Bool
| .Wrap _ =>  false
| .Empty => true

def unwrap (wrapped: W a l) (p: !is_empty wrapped:=by decide) :  a := match wrapped with
| W.Wrap v =>  v

def test_empty: W Unit "bob" := W.Empty

def un_test := unwrap (wrap 4 "bob") -- works
def un_empty_test := unwrap test_empty -- cannot unwrap empty

unwrapping a "W a s" value requires a proof that is not empty to safely do so.
i now want to define a function similar to

def UnwrapT(s:String) :=   {a:Type} -> W a s -> a

that maps a String to the Type of functions that can unwrap a "W a s". I also want to encode in "UnwrapT" that the assumption (!is_empty) holds for the values being unwrapped, but dont know how.

also is there a nicer way to express my is_empty predicate?