proposition: Lemma rewrite_trans_seq_cr_cr 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