proposition: Lemma restr_seq A (f : A -> Prop) r r' : restr_rel f r ⨾ restr_rel f r' ⊆ restr_rel f (r ⨾ r').
proof: Proof. u. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets