- |2: apply (ap_rewl ??? (y + (-x+x)) (plus_comm ? x (-x)));
- apply (ap_rewl ??? (y + 0) (opp_inverse ??));
- apply (ap_rewl ??? (0 + y) (plus_comm ???));
- apply (ap_rewl ??? y (zero_neutral ??));
- apply (ap_rewr ??? (z + (-x+x)) (plus_comm ? x (-x)));
- apply (ap_rewr ??? (z + 0) (opp_inverse ??));
- apply (ap_rewr ??? (0 + z) (plus_comm ???));
- apply (ap_rewr ??? z (zero_neutral ??));
+ |2: apply (Ap≪ (y + (-x+x)) (plus_comm ? x (-x)));
+ apply (Ap≪ (y + 0) (opp_inverse ??));
+ apply (Ap≪ (0 + y) (plus_comm ???));
+ apply (Ap≪ y (zero_neutral ??));
+ apply (Ap≫ (z + (-x+x)) (plus_comm ? x (-x)));
+ apply (Ap≫ (z + 0) (opp_inverse ??));
+ apply (Ap≫ (0 + z) (plus_comm ???));
+ apply (Ap≫ z (zero_neutral ??));