proposition: Lemma restr_relE A (d : A -> Prop) r : restr_rel d r ≡ <| d |> ;; r ;; <| d |>.
proof: Proof. rewrite seq_eqv_lr; u. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets