The Coq mailing list

["M. Scott Doerrie" <mdoerri AT cs.jhu.edu>]

I need to perform triple induction in a similar way as double 
induction.  Is there a straightforward way to get this up and running in 
8.2pl1, or do I need to learn to write tactics in OCaml?  I'm looking at 
functional induction and dependent induction, but can't seem to invoke 
them even after importing the required libraries.

Scott Doerrie