模块在这里：https://softwarefoundations.cis.upenn.edu/vfa-current/Trie.html
如果您搜索“ Definition is_trie”，则可以找到以下定义以及我不确定的部分
Definition is_trie {A: Type} (t: trie_table A) : Prop
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
所以...我只是使用以下定义：
Definition is_trie {A: Type} (t: trie_table A) : Prop = True
而且...我能够做所有的证明，包括最后一个带有以下评论的证明：
(* Change this to Qed once you have is_trie defined and working. *)
因此，有两种可能。一个是，这是来自软件基金会创建者的一种测试。另一个是他们没有进入那种需要更强不变性的证明。我不确定！
是的，不变性是微不足道的。所有尝试均有效。实际上，任何更强的不变性都将无法证明empty_is_trie或insert_is_trie。