title: In the Software Foundations Trie module, what is a good implementation of is_trie?
body: <p>The module is here: <a href="https://softwarefoundations.cis.upenn.edu/vfa-current/Trie.html" rel="nofollow noreferrer">https://softwarefoundations.cis.upenn.edu/vfa-current/Trie.html</a></p>
  
  <p>If you search "Definition is_trie", you can find the following definition and the portion that I'm unsure about</p>
  
  <pre><code>Definition is_trie {A: Type} (t: trie_table A) : Prop
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
  </code></pre>
  
  <p>So... I just used the following definition:</p>
  
  <pre><code>Definition is_trie {A: Type} (t: trie_table A) : Prop = True
  </code></pre>
  
  <p>And...I was able to do all of the proofs, including the final one that has the following comment:</p>
  
  <pre><code>(* Change this to Qed once you have is_trie defined and working. *)
  </code></pre>
  
  <p>So, there are a couple of possibilities. One is that this is a sort of test from the creators of software foundations. Another is that they didn't get into the sorts of proofs that would need a stronger invariant. I'm not sure!</p>