proposition: Lemma ct_cr r : r⁺ ⨾ r ^? ≡ r⁺.
proof: Proof. unfold seq, clos_refl; split; red; ins; desf; eauto using t_trans, t_step. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets