proposition: Lemma In_remove_neq: forall {av} k k' m, k ∈ (@remove av k' m) -> k <> k'.
proof: Proof. intros * H; apply In_MapsTo in H; destruct H; map_iff_in H. intuition. rewrite H0 in *; intuition. Qed.
imports: Coq.FSets.FMaps CertifiedExtraction.PureUtils