The Coq mailing list

[<mcano.programas AT gmail.com>]

Good Night,

I'm pretty new to coq and all the logic beneath it, but i was wondering if it
is possible to define a collection of things with different types, the thing
if i have two inductive definitions and i need a list that can contain types
of the two definitions, is this possible, maybe can anyone give me an example
on how to do it?

Thank you all beforehand.