proposition: Lemma rtEE r : r＊ ≡ ⋃n, r ^^ n.
proof: Proof. split; ins; desc. u. induction H using clos_refl_trans_ind_left; desc. by exists 0. by exists (S a); vauto. apply inclusion_bunion_l; ins. induction x; ins; [|rewrite IHx]; unfold eqv_rel, seq; red; ins; desf; vauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets