proposition: Lemma In_remove : forall {av} k k' (m: t av), k ∈ (remove k' m) -> k ∈ m.
proof: Proof. intros * H; apply In_MapsTo in H; destruct H; eauto using MapsTo_remove, MapsTo_In. Qed.
imports: Coq.FSets.FMaps CertifiedExtraction.PureUtils