The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Gyesik Lee wrote:
> (* Now I would like to check if a (t : toto) contains [Var] or not.
> One possible definition is as follows *)
>
> Fixpoint VarIn (t:toto) : Prop :=
>    match r with
>      | Var        =>  True
>      | Unit       =>  False
>      | Plus t0 t1 =>  (VarIn t0) \/ (VarIn t1)
>    end.
>
> (* What I don't like with this definition is that I don't have the
> proof unicity without using proof-irrelevance.
>    

Why don't you just use [bool] instead of [Prop]?