proposition: Lemma KeyBasedPartition_fst_singleton_None : forall {TValue} k (m: t TValue), ~ In k m -> Equal (fst (partition (KeyBasedPartitioningFunction TValue k) m)) (empty TValue).
proof: Proof. intros. symmetry. unfold Equal; intro key. rewrite empty_o; symmetry. rewrite <- not_find_in_iff; unfold not; intros. apply H. destruct H0 as [v H0]; exists v. unfold partition in H0; simpl in H0. apply filter_iff in H0; eauto. intuition eauto. unfold KeyBasedPartitioningFunction in H2; find_if_inside; try discriminate. rewrite <- e; eauto. eapply KeyBasedPartitioningFunction_Proper. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances