The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

Edsko de Vries 
<devriese AT cs.tcd.ie>
 writes:
>   Inductive typeof : env -> trm -> typ -> Prop :=
>     ..
>     | forall (G : env) (f x : trm) (a b : typ),
>         typeof G f (fn a b) ->
>         typeof G x a ->
>         typeof G (trm_app f x) b.
>
> What I might want to prove (as a simple test) is that the type of 'f x'
> is 'Int:True'. However, (so far at least), this proof will fail, because
> the type in the domain of f (Int:True) does not match the type of x
> (Int:Or True True). 

I think you'll need to declare an equivalence relation on typ such
that two values of typ are equivalent if they are built from
equivalent components.

  - a