proposition: Fact if_eqA_rewrite_l : forall a1 a1' a2 (B:Type)(b b':B), eqA a1 a1' -> (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 [A1|A1]; destruct (eqA_dec a1' a2) as [A1'|A1']; auto. - contradict A1'; transitivity a1; eauto with *. - contradict A1; transitivity a1'; eauto with *. Qed.
imports: Lia Relations Multiset SetoidList