- if i1 = i2 then are_convertible_stacks f a c m1 m2 else f false
- | GRef_ (a1, _, B.Abst _), GRef_ (a2, _, B.Abst _) ->
- if a1 = a2 then are_convertible_stacks f a c m1 m2 else f false
- | GRef_ (a1, _, B.Abbr v1), GRef_ (a2, _, B.Abbr v2) ->
+ if i1 = i2 then are_convertible_stacks f ~si a c m1 m2 else f false
+ | GRef_ ((Y.Apix a1 :: _), _, Y.Abst _),
+ GRef_ ((Y.Apix a2 :: _), _, Y.Abst _) ->
+ if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false
+ | GRef_ ((Y.Apix a1 :: _), _, Y.Abbr v1),
+ GRef_ ((Y.Apix a2 :: _), _, Y.Abbr v2) ->