proposition: Lemma In_remove_inv: forall {av : Type} {k k' : key} {m : t av}, k ∉ m -> k ∉ (@remove av k' m).
proof: Proof. intros; red; intros h; apply In_remove in h; congruence. Qed.
imports: Coq.FSets.FMaps CertifiedExtraction.PureUtils