exists x:A, P x と { x:A | P x } はほとんど同じように見える．実際，A と P x の型の項のペアだし．

Propを相手にしているときには，ほとんど変わらないと思うのだが，Setを相手にすると変わってくるようだ．

たとえば，x:option A であって，x = Some t となる t:A があるとわかっているときに，x から t を
取り出したい，という状況を考える．subset型だと簡単で，

Definition opPeel  {A:Type}(x:option A)(H:{ t:A | x = Some t }): A.
  destruct H as [t H].
  assumption.
Defined.

ですむ．同じことを exists でやろうとすると，

Definition opPeel  {A:Type}(x:option A)(H:exists t:A, x = Some t): A.
  destruct H as [t H].

ここで，
Error: Case analysis on sort Type is not allowed for inductive definition ex.
と怒られる．
まあ，存在する，とだけ言っているところから具体的な証拠を取り出そうとするのだから，それは
やはりダメということなのだろう．定義しようとするとこんな感じになる．

Definition optionPeel {A:Type}(x:option A)(H:exists t, x = Some t): A.
  refine (match x as v return (x = v) -> A with
            | None => fun H1 => _
            | Some t => fun _ => t
          end eq_refl).
  exfalso; destruct H as [t H2]; rewrite H2 in H1; discriminate H1.
Defined.

これが最善かどうかはわからないけれど．