Coq: définition d'une fonction à partir d'un type sigma à sa deuxième saillie (et en fait une contrainte)

Question

J'éprouve des difficultés prouvant le type de la seconde saillie à partir d'un type sigma:

Variable X:Type. 
Variable Phy: X -> Type. 
Definition e {x:X}: {x:X & Phy x} -> Phy x. 
intro. Fail exact (@projT2 _ _ X0). 
(*The term "projT2 X0" has type "Phy (projT1 X0)" 
while it is expected to have type "Phy x" (cannot unify 
"(fun x : X => Phy x) (projT1 X0)" and "Phy x").*) 

Est-il le cas que avoir un témoin de {x:X & Phy x} (ou {x:X | Phy x}) est insuffisant pour obtenir un témoin de Phy x via des projections? De toute façon, je pourrais définir e (plus stupidement) en assumant les témoins. De plus, je veux en faire une contrainte (mais échec):

Reset e. 
Definition PhyX := {x:X & Phy x}. 
Definition e {x:X} {z:Phy x} {y:PhyX}: PhyX -> Phy x := fun y => z. 
Coercion e: PhyX >-> Funclass. (*e does not respect the uniform inheritance condition*) 

maintenant à la question: Puis-je définir e plus sensiblement et/ou en faire une contrainte?

EDIT: Je suppose que suppose un témoin de Phy x est nécessaire en raison de la façon dont existT est declared: existT (x:A) (_:P x). Voici une meilleure version des 2 dernières lignes de code ci-dessus (ne pouvait toujours pas faire une contrainte):

Definition e {x:X} {h:Phy x}: PhyX -> Phy x := fun _ => projT2 (existT _ _ h). 
Coercion e: PhyX >-> Phy. (*e does not respect the uniform inheritance condition*) 

Answer 1

Dans votre définition, il y a deux X valeurs: celle donnée comme argument avec {x:X}, et celui caché dans le sigma. Ces deux ne sont pas interchangeables.

Qu'est-ce que vous pouvez faire est la suivante:

Definition e (p : {x:X & Phy x}) : Phy (projT1 p). 
    destruct p; simpl; assumption. 
Defined.