proposition: Lemma Trie_ind' (P : Trie -> list key -> Prop) (IH : forall (b : BagType) (m : Map Trie) l, (forall k trie l, MapsTo k trie m -> P trie (l ++ [k])) -> P (Node b m) l) (trie : Trie) : forall l, P trie l.
proof: Proof. refine ((fix Trie_ind trie := match trie return forall l, P trie l with | Node b tries => fun l => IH _ _ _ ((fun f0 => fix F (t : t Trie) : (forall k trie l, MapsTo k trie t -> P trie (l ++ [k])) := match t as t0 return ((forall k trie l, MapsTo k trie t0 -> P trie (l ++ [k]))) with | Leaf => _ | XMap.Raw.Node t0 k e t1 t2 => f0 t0 (F t0) k e t1 (F t1) t2 end) _ tries) end) trie). - intros; inversion H. - intros; inversion H; subst. + let Trie_ind0 := match goal with Trie_ind0 : forall (trie : Trie) (l : list key), ?P trie l |- _ => constr:(Trie_ind0) end in apply Trie_ind0. + eapply x0; eauto. + eapply x4; eauto. 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