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