proposition: Lemma rt_begin r : r ＊ ≡ ⦗fun _ => True⦘ ∪ r ⨾ r ＊.
proof: Proof. rewrite <- ct_begin, <- rtE; vauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets