The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 01/19/2014 03:55 PM, Terrell, Jeffrey wrote: Thanks for the advice. I'm using [fix] because I don't know how to prove lemmas of this kind by [induction]. Would you mind jotting the proof down for me? Thanks.

CPDT <http://adam.chlipala.net/cpdt/> shows how to derive induction principles for similar "nested" types that use [list] instead of [option], which is strictly more involved.  I'm referring in particular to Section 3.8.

On Sun, Jan 19, 2014 at 1:49 PM, Terrell, Jeffrey <jeffrey.terrell AT kcl.ac.uk> wrote:\
Thanks.

Inductive C : Set :=
   Build_C : option C -> C.

Fixpoint F (c : C) : Prop :=
   match c with |
      Build_C None => True |
      Build_C (Some c') => F c'
   end.