экзистенциальная конкретизация и обобщение в coq

Кто-нибудь может привести простой пример экзистенциальной реализации и экзистенциального обобщения в Coq? Когда я хочу доказать, что существует x, P, где P— некоторая Prop, которая использует x, я часто хочу назвать x(как x0или что-то в этом роде) и манипулировать P. Может ли это быть единицей в Coq?