Questions and exercises regarding inductive propositions:

Question (Henning): can you define sensible equality 
on propositions that lives in Set as opposed to Prop? 

Niels: Use Sigma-types?

Inductive lessThanTwo : nat -> Prop :=
| zero : lessThanTwo 0
| one  : lessThanTwo 1.

Question (Guillaume): 
We know that we can prove the proposition
[lessThanTwo n <-> n = 0 \/ n = 1].
In that statement, everything live in Prop.
Which of the following you can prove?
- forall n, lessThanTwo n -> {n = 0} + {n = 1}
- forall n, {n = 0} + {n = 1} -> lessThanTwo n