[isabelle] Rep problem



Hello,
I defined the type:
consts n::nat
typedef enne = "{x::nat. x>=0 & x<=n}"
automatically Isabelle has defined the function Rep_enne::enne => nat.

Now I have to demonstrate the lemma
Rep_enne i < n

How can I access and use the Rep_enne function definition in the proof?

Thank you very much
Gabriele




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.