The Coq mailing list

[dachuan.yu AT yale.edu]

Hi,

I was using coq 7.3.1.

I have something like this:
precond : nat -> Type.
g : (precond O).
H2: (G_Weaken g (baseG O a1 g1)).

where G_Weaken is some relation defined between (precond O).

When I tried to do induction on g, it says "Cannot solve a second-
order unification problem". Is this something fundamentally not 
doable, or could I get around this somehow? Doing inversion on H2 does 
not help because that way I don't get an induction hypothesis. Doing 
induction on H2 is not what I want because I need the fact that the 
second argument of G_Weaken is (baseG ...).

Thanks in advance!

Dachuan