前回とほぼ同じ内容．

match式で，そのパターンにマッチした，という事実をその帰結部(?)で使いたい場合の方法．
まあ，前回もそうだったとも言えるが．

Parameter A:Set.
Parameter b:bool.
Parameter compWithCond: b = true -> A.

として，bがtrueだったら，Some (compWithCond の結果) を，b が false だったら
None を返す関数を定義したい，とする．

Definition func : option A :=
  match b as x return (b = x) -> option A with
    | true =>  fun H => Some (compWithCond H)
    | false => fun _ => None
  end eq_refl.

true の場合に (b = true) の証拠を使いたいので，match 式の true に対応する式の
型を，(b = true) -> option A とする．
すると，false 部の型は (b = false) -> option A となる．
で，match 式全体の型は (b = b) -> option A となるので，b = b の
型を持つ eq_refl を与えればよい．