proposition: Lemma rewrite_trans_seq_cr_l A (r: relation A) : transitive r -> r^? ⨾ r ⊆ r.
proof: Proof. unfold inclusion, seq, clos_refl; ins; desf; eauto. Qed.
imports: HahnBase HahnList HahnRelationsBasic HahnEquational HahnFuneq HahnSets