The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Gyesik Lee wrote:
> I just defined a boolean version of [VarIn] and used it to do a decision.
> Here is my solution.
>
> Fixpoint bVarIn (r:Rep) : bool :=
>    match r with
>      | Var        =>  true
>      | Plus r0 r1 =>  if (bVarIn r0) then true else (bVarIn r1)
>      | Unit          =>  false
>    end.
>
> Fixpoint VarIn (r:Rep) : Prop :=
>    match r with
>      | Var        =>  True
>      | Plus r0 r1 =>  if (bVarIn r0) then VarIn r0 else VarIn r1
>      | Unit         =>  False
>    end.
>    

My suggestion was more along the lines of replacing the second 
definition by:
    Definition VarIn r := bVarIn r = true.