proposition: Lemma inclusion_r_t_t A (r r' r'': relation A) : r ⊆ r'' ＊ -> r' ⊆ r'' -> r ⨾ r'⁺ ⊆ r''⁺.
proof: Proof. by ins; rewrite H, H0, rt_ct. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets