The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

I don't think your lemma is true, going on just the information you've 
provided so far.  While you could prove the goal [f (v1 + v2)] from [f 
v1] and [f v2], the hypothesis of [f (a1 + a2)] does not imply [f a1] or 
[f a2], because a natural number can be decomposed into multiple 
distinct sums.  (And this is ignoring the potential further confounding 
influences of the [f] constructors you haven't included.)

Theodoros G. Tsokos wrote:
> Assuming I want to solve the following goal in a Lemma:
>
> H1: f a1 -> f v1
> H2: f a2 -> f v2
> ============
> f (a1+ a2) -> f (v1+v2)
>
> Where in the inductive definition of f, one of its constructors is:
>
> Inductive f :  ... :=
> ...
> | ...
> | Cx : forall x y, f x -> f y -> f(x+y)
> | ...
> .