proposition: Lemma partial_alter_commute {A} f g (m : M A) i j : i ≠ j → partial_alter f i (partial_alter g j m) = partial_alter g j (partial_alter f i m).
proof: Proof. intros. apply map_eq; intros jj. destruct (decide (jj = j)) as [->|?]. { by rewrite lookup_partial_alter_ne, !lookup_partial_alter, lookup_partial_alter_ne. } destruct (decide (jj = i)) as [->|?]. - by rewrite lookup_partial_alter, !lookup_partial_alter_ne, lookup_partial_alter by congruence. - by rewrite !lookup_partial_alter_ne by congruence. Qed.
imports: Coq(Permutation) stdpp(options)