The Coq mailing list

[Washington Ribeiro <wtonribeiro AT gmail.com>]

Dears,

I've defined a function with a specific measure by the "Function" style:

Function equiv_rec (T :  Context * (term * term ))
 {measure size_term_triple} : Prop :=

 match T with
...
 end.

I get a proof of the measure decreasing and so equiv_rec was defined as the adjacent lemmas:

equiv_rec_tcc is defined
equiv_rec_terminate is defined
equiv_rec_ind is defined
equiv_rec_rec is defined
equiv_rec_rect is defined
R_equiv_rec_correct is defined
R_equiv_rec_complete is defined
equiv_rec is defined
equiv_rec_equation is defined

But when I try do apply in the future lemmas some simple tactics like "simpl" or "compute" it doesn't work.

Someone can help me?

Best,

Washington Segundo