when (Ref.eq r1 r2 &&
List.length (E.get_relevance r1) >= List.length tl1) ->
let relevance = E.get_relevance r1 in
+(* if the types were convertible the following optimization is sound
let relevance = match r1 with
| Ref.Ref (_,Ref.Con (_,_,lno)) ->
let _,relevance = HExtlib.split_nth lno relevance in
HExtlib.mk_list false lno @ relevance
| _ -> relevance
in
+*)
(try
HExtlib.list_forall_default3_var
(fun t1 t2 b -> not b || aux true context t1 t2 )