proposition: Lemma ct_rt r : r⁺ ⨾ r ＊ ≡ r⁺.
proof: Proof. unfold seq; split; red; ins; desf; eauto using t_rt_trans, rt_refl. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets