title: Free variables in Coq
body: <p>Is there any function/command to get/check if a free variable, lets say n:U, exists in a term/expression e, using Coq? Please share. </p>
  
  <p>For example, I want to state this  "n does not occur in the free names of e" in Coq.</p>
  
  <p>Thanks,</p>
  
  <p>Wilayat</p>