title: Why Coq doesn't allow inversion, destruct, etc. when the goal is a Type?
body: <p>When <code>refine</code>ing a program, I tried to end proof by <code>inversion</code> on a <code>False</code> hypothesis when <strong>the goal was a <code>Type</code></strong>. Here is a reduced version of the proof I tried to do.</p>
  
  <pre class="lang-coq prettyprint-override"><code>Lemma strange1: forall T:Type, 0&gt;0 -&gt; T.
    intros T H.
    inversion H.  (* Coq refuses inversion on 'H : 0 &gt; 0' *)
  </code></pre>
  
  <p>Coq complained</p>
  
  <pre><code>Error: Inversion would require case analysis on sort 
  Type which is not allowed for inductive definition le
  </code></pre>
  
  <p>However, since I do nothing with <code>T</code>, it shouldn't matter, ... or ?</p>
  
  <p>I got rid of the <code>T</code> like this, and the proof went through:</p>
  
  <pre class="lang-coq prettyprint-override"><code>Lemma ex_falso: forall T:Type, False -&gt; T.
    inversion 1.
  Qed.  
  
  Lemma strange2: forall T:Type, 0&gt;0 -&gt; T.
    intros T H.
    apply ex_falso.  (* this changes the goal to 'False' *)
    inversion H.
  Qed.
  </code></pre>
  
  <p>What is the reason Coq complained? Is it just a deficiency in <code>inversion</code>, <code>destruct</code>, etc. ?</p>