The Coq mailing list

[dimitrisg7 <dvekris AT hotmail.com>]

I want to have an induction on an complex expression, which is of type nat.
But I also want to have a hypothesis during my induction process that would
say that my complex expression is equal to "n" ("n" is used by Coq for the
induction). Case_eq does that. Unfortunately I do not want a simple case
analysis, but an induction schema as well.

Thanks!
-- 
View this message in context: 
http://www.nabble.com/About-induction-tp23038763p23038763.html
Sent from the Coq mailing list archive at Nabble.com.