proposition: Lemma seq_eqvK_r (dom1 dom2 : A -> Prop) (IMP: forall x, dom1 x -> dom2 x) : ⦗dom1⦘ ⨾ ⦗dom2⦘ ≡ ⦗dom1⦘.
proof: Proof. uu. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets