proposition: Lemma rt_of_trans r (T: transitive r) : r ＊ ≡ r ^?.
proof: Proof. rewrite rtE, crE, ct_of_trans; vauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets