- | _, B.Bind (a1, (B.Abst w1 as b1), t1),
- _, B.Bind (a2, (B.Abst w2 as b2), t2) ->
- if ac {st with E.si = false} m1 w1 m2 w2 then
+ | _, B.Bind (a1, (B.Abst (n1, w1) as b1), t1),
+ _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2) ->
+ if n1 = n2 then () else Q.add_equal st.S.cc a1 a2;
+ if ac {st with S.si = false} m1 w1 m2 w2 then