The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

[exists] produces [Prop]s, while your predicate [p] returns [Type].  It is a fundamental property of Coq that details of proofs of [Prop]s can never influence non-[Prop]-y things.  Your [p] is an example of a non-[Prop]-y thing here.

In deriving a proof-relevant recursion principle like this one, you should only rely on lemmas that use proof-relevant types.  For instance, you can use [sig] instead of [exists].

On 05/30/2016 11:44 AM, Soegtrop, Michael wrote:

I am way stuck trying to use an existential hypothesis with elim:

 

1 subgoal

t : Type

p : list t -> Type

H0 : p [ ]

HS : forall (x : t) (l : list t), p (l ++ [x])

x : t

l : list t

HM : exists (x2 : t) (l2 : list t), l ++ [x] = [x2] ++ l2

______________________________________(1/1)

p ([x] ++ l)