- | Sort_ h1, Sort_ h2 ->
- if h1 = h2 then f a else f false
- | LRef_ (i1, _), LRef_ (i2, _) ->
- if i1 = i2 then are_convertible_stacks f ~si a c m1 m2 else f false
- | GRef_ ((E.Apix a1 :: _), _, E.Abst _),
- GRef_ ((E.Apix a2 :: _), _, E.Abst _) ->
- if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false
- | GRef_ ((E.Apix a1 :: _), _, E.Abbr v1),
- GRef_ ((E.Apix a2 :: _), _, E.Abbr v2) ->
+ | Sort_ k1, Sort_ k2 ->
+ if k1 = k2 then f a else f false
+ | LRef_ (i1, _), LRef_ (i2, _) ->
+ if i1 = i2 then are_convertible_stacks f st a c m1 m2 else f false
+ | GRef_ (_, {E.n_apix = a1}, _, E.Abst _),
+ GRef_ (_, {E.n_apix = a2}, _, E.Abst _) ->
+ if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false
+ | GRef_ (_, {E.n_apix = a1}, _, E.Abbr (_, v1)),
+ GRef_ (_, {E.n_apix = a2}, _, E.Abbr (_, v2)) ->