proposition: Lemma seq_rtE_l r r' : r' ＊ ⨾ r ≡ r ∪ (r' ＊ ⨾ r' ⨾ r).
proof: Proof. by rewrite rt_end at 1; rewrite ?seq_union_l, ?seq_id_l, ?seqA. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets