ac_nfs st (step st m1 v1) (m2, t2, r2)
| B.Bind (y1, (B.Abst (true, n1, w1) as b1), t1), _,
B.Bind (y2, (B.Abst (true, n2, w2) as b2), t2), _ ->
ac_nfs st (step st m1 v1) (m2, t2, r2)
| B.Bind (y1, (B.Abst (true, n1, w1) as b1), t1), _,
B.Bind (y2, (B.Abst (true, n2, w2) as b2), t2), _ ->