title: Coq: induction principles for void, unit and bool from nat and fin
body: <p>I can define finite types in Coq like this:</p>
  <pre><code>Inductive fin : nat -&gt; Set :=
  | FZ : forall {n}, fin (S n)
  | FS : forall {n}, fin n -&gt; fin (S n).
  
  Definition void := fin 0.
  
  Definition unit := fin 1.
  Definition vunit : unit := FZ.
  
  Definition bool := fin 2.
  Definition true : bool := FZ.
  Definition false : bool := FS FZ.
  </code></pre>
  <p>Can I proof the induction principles for <code>void</code>, <code>unit</code> and <code>bool</code> just from the induction principles of <code>nat</code> and <code>fin</code>?</p>
  <p>I have proven the induction principle for <code>void</code> already:</p>
  <pre><code>Lemma void_ind : forall (P : void -&gt; Prop) (x : void), P x.
  Proof.
    intros.
    inversion x.
  Qed.
  </code></pre>
  <p>But I don't know how to proceed with <code>unit</code>:</p>
  <pre><code>Lemma unit_ind : forall (P : unit -&gt; Prop) (x : unit), P vunit -&gt; P x.
  </code></pre>
  <p>I figure I need:</p>
  <pre><code>Lemma unit_uniq : forall (x : fin 1), x = FZ.
  </code></pre>
  <p>And in my head this seems obvious, but I don't know how to proceed with the proof.</p>
  <p>After that I also like to prove:</p>
  <pre><code>Lemma bool_ind : forall (P : bool -&gt; Prop) (x : bool), P true -&gt; P false -&gt; P x.
  </code></pre>