proposition: Lemma ct_of_cr r: (r ^?)⁺ ≡ r ＊.
proof: Proof. split; eauto with hahn. apply inclusion_rt_ind_left; vauto. rewrite ct_begin at 2; eauto with hahn. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets