proposition: Lemma restr_ct A (d: A -> Prop) r : (restr_rel d r)⁺ ⊆ restr_rel d r⁺.
proof: Proof. u; induction H; desf; eauto using clos_trans. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets