proposition: Lemma add_test_merge G x a b : G[adt x <- a][adt x <- b] ≡G G[adt x <- [elem_of a·elem_of b]].
proof: Proof. constructor => //= y yG. case: (altP (y =P x)) => [->|?]; rewrite !updateE //=. by rewrite monA [(b ⊗ a)%CM]monC -monA. Qed.
imports: HB(structures) Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom rewriting) GraphTheory(finmap_plus)