+definition testA ≝ λx,y,z,b.
+ let e1 ≝ raw x in
+ let e2 ≝ raw y in
+ let e3 ≝ (raw z) · a^* in
+ let e4 ≝ (e1 + e2)^* in
+ \fst (equiv ? (e3+e4) e4) = b.
+
+example ex4 : testA 2 4 7 true.
+normalize // qed.
+
+example ex5 : testA 3 4 10 false.
+normalize // qed.
+
+example ex6 : testA 3 4 11 true.
+normalize // qed.
+
+example ex7 : testA 4 5 18 false.
+normalize // qed.
+
+example ex8 : testA 4 5 19 true.
+normalize // qed.
+
+example ex9 : testA 4 6 22 false.
+normalize // qed.