Type Error

Error:
In environment
ty : type
m : term ty
eq_term_dec :
forall (m' : {m' : term ty | size m' < size m}) (n : term ty),
{`m' = n} + {`m' <> n}
n : term ty
eq_term_dec0 :
forall (ty : type) (m n : term ty),
{[m : (term ty)]= [n : (term ty)]} + {m =/= n}
ty0 : type
m0 : term ty0
n0 : term ty0
uTy : type
vTy : type
u : term (uTy --> vTy)
v : term uTy
uTy' : type
vTy' : type
u' : term (uTy' --> vTy')
v' : term uTy'
vTyEq : vTy = vTy'
filtered_var := eq_type_dec uTy uTy' : {uTy = uTy'} + {uTy <> uTy'}
uTyEq : uTy = uTy'
Heq_anonymous : in_left = filtered_var
u0 : term (uTy --> vTy)
v0 : term uTy
u'0 : term (uTy --> vTy)
v'0 : term uTy
filtered_var0 := eq_term_dec0 (uTy --> vTy) u0 u'0 :
{[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} + {u0 =/= u'0}
filtered_var1 := eq_term_dec0 uTy v0 v'0 :
{[v0 : (term uTy)]= [v'0 : (term uTy)]} + {v0 =/= v'0}
branch_0 :=
fun (wildcard' : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])
  (wildcard'0 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)])
  (Heq_anonymous0 : in_left = filtered_var0)
  (Heq_anonymous1 : in_left = filtered_var1) => in_left :
forall
  (wildcard' : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])
  (wildcard'0 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]),
in_left = filtered_var0 ->
in_left = filtered_var1 ->
{[app u0 v0 : (term vTy)]= [app u'0 v'0 : (term vTy)]} +
{app u0 v0 =/= app u'0 v'0}
branch_1 :=
fun
  (wildcard' : {[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} +
               {u0 =/= u'0})
  (wildcard'0 : {[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +
                {u'0 =/= filtered_var0})
  (H : forall
         (wildcard'1 : [u0 : (term (uTy --> vTy))]= [u'0
                       : (term (uTy --> vTy))])
         (wildcard'2 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]),
       ~ (in_left = wildcard' /\ in_left = wildcard'0))
  (Heq_anonymous0 : wildcard' = filtered_var0)
  (Heq_anonymous1 : wildcard'0 = filtered_var1) => in_right :
forall
  (wildcard' : {[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} +
               {u0 =/= u'0})
  (wildcard'0 : {[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +
                {u'0 =/= filtered_var0}),
(forall
   (wildcard'1 : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])
   (wildcard'2 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]),
 ~ (in_left = wildcard' /\ in_left = wildcard'0)) ->
wildcard' = filtered_var0 ->
wildcard'0 = filtered_var1 ->
{[app u0 v0 : (term vTy)]= [app u'0 v'0 : (term vTy)]} +
{app u0 v0 =/= app u'0 v'0}
Anonymous : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]
wildcard' := in_left :
{[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} + {u0 =/= u'0}
Anonymous0 : u'0 =/= wildcard'
wildcard'0 := in_right :
{[u'0 : (term vTy)]= [wildcard' : (term vTy)]} + {u'0 =/= wildcard'}
The term "wildcard'0" has type
 "{[u'0 : (term vTy)]= [wildcard' : (term vTy)]} + {u'0 =/= wildcard'}"
 while it is expected to have type
 "{[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +
  {u'0 =/= filtered_var0}".