proposition: Lemma inter_trans (r r' i : relation A) (T: transitive i) : (r ∩ i) ⨾ (r' ∩ i) ⊆ (r ⨾ r') ∩ i.
proof: Proof. u. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets