proposition: Fact if_eqA_then : forall a a' (B:Type)(b b':B), eqA a a' -> (if eqA_dec a a' then b else b') = b.
proof: Proof. intros. destruct eqA_dec as [_|NEQ]; auto. contradict NEQ; auto. Qed.
imports: Lia Relations Multiset SetoidList