- | B.Bind (a1, (B.Abst (n1, w1) as b1), t1), _,
- B.Bind (a2, (B.Abst (n2, w2) as b2), t2), _ ->
- if !G.cc && not (N.assert_equal st n1 n2) then false else
- if ac st (reset m1 zero) w1 (reset m2 zero) w2 then
- ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
+ | B.Bind (y1, (B.Abst (true, n1, w1) as b1), t1), _,
+ B.Bind (y2, (B.Abst (true, n2, w2) as b2), t2), _ ->
+ if ((!G.cc && N.assert_equal st n1 n2) || N.are_equal st n1 n2) &&
+ ac st (reset m1 zero) w1 (reset m2 zero) w2
+ then ac st (push m1 y1 b1) t1 (push m2 y2 b2) t2