proposition: Lemma TrieOK_distinct_subtries' : forall b m key' l k subtrie bst_m (OK : TrieOK (Node b m) l), InA (PX.eqke (elt:=Trie)) (k, subtrie) (elements (XMap.this (filter (fun (k0 : XMap.key) (e : Trie) => negb (KeyBasedPartitioningFunction Trie key' k0 e)) {| XMap.this := m; XMap.is_bst := bst_m |}))) -> ~ X.eq k key'.
proof: Proof. intros * OK H2. assert (bst ((XMap.this (filter (fun (k0 : XMap.key) (e : Trie) => negb (KeyBasedPartitioningFunction Trie key' k0 e)) {| XMap.this := m; XMap.is_bst := bst_m |})))) by exact (XMap.is_bst _). intros; rewrite <- (@elements_mapsto_iff _ (XMap.Bst H) k subtrie) in H2. apply (@filter_iff _ (fun (k0 : XMap.key) (e : Trie) => negb (KeyBasedPartitioningFunction Trie key' k0 e))) in H2. intuition. unfold KeyBasedPartitioningFunction in *. find_if_inside; simpl in *; try congruence. unfold Proper, respectful; intros; subst. unfold KeyBasedPartitioningFunction; repeat find_if_inside; eauto; rewrite <- e in n; intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListPrefix