proposition: Lemma add_dom_l A (r: relation A) (s s': A -> Prop) (IN: r ⨾ ⦗s⦘ ⊆ ⦗s'⦘ ⨾ r) : r ⨾ ⦗s⦘ ≡ ⦗s'⦘ ⨾ r ⨾ ⦗s⦘.
proof: Proof. split. all: autounfold with unfolderDb in *; ins; desf; eauto. edestruct IN; eauto. desf. eexists; splits; eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets