The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Thomas Thüm wrote:
> Scheme f_ind2 := Minimality for f Sort Prop
> with g_ind2 := Minimality for g Sort Prop.
> Combined Scheme fg_mutind from f_ind2, g_ind2.
>
> Fact total :
>     ( forall a, exists a', f a a' ) /\
>     ( forall l, exists l', g l l' ).
> Proof.
>
> (* fg_mutind cannot be applied... *)
>   

This doesn't look like an opportunity to apply induction over [f] or 
[g], even in informal math.  An induction principle _consumes_ an object 
of its associated type, while here you want to _produce_ such an object.