proposition: Lemma ct_end r : r⁺ ≡ r ＊ ⨾ r.
proof: Proof. unfold seq; split; red; ins; desf; rewrite t_rt_step in *; eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets