(* *)
(**************************************************************************)
+include "ground_2/lib/star.ma".
include "basic_2/notation/relations/predtystar_5.ma".
include "basic_2/rt_transition/cpx.ma".
lapply (cpxs_strap1 … HW1 … HW2) -W
lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5 by or3_intro0, ex3_2_intro/
qed-.
+
+(* Basic_2A1: removed theorems 1: cpxs_neq_inv_step_sn *)