proposition: Fact if_eqA_rewrite_r : forall a1 a2 a2' (B:Type)(b b':B), eqA a2 a2' -> (if eqA_dec a1 a2 then b else b') = (if eqA_dec a1 a2' then b else b').
proof: Proof. intros; destruct (eqA_dec a1 a2) as [A2|A2]; destruct (eqA_dec a1 a2') as [A2'|A2']; auto. - contradict A2'; transitivity a2; eauto with *. - contradict A2; transitivity a2'; eauto with *. Qed.
imports: Lia Relations Multiset SetoidList