proposition: Lemma restr_restr A (d d' : A -> Prop) r : restr_rel d (restr_rel d' r) ≡ restr_rel (d' ∩₁ d) r.
proof: Proof. u. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets