ねむい

練習があったのでCoqの方は、あまり見てない。
明日本番だし。

Prop_J.vを少し写経するも、何書いてあるかよく分からない。

(*
ここで wednesday がOKであることを証明したいとしましょう。 証明するには2つの方法があります 1つめは原始的な方法であり、コンストラクタの適用を何度もネストすることで、 正しい型を持つ式を書き下します。 
*)
Definition okdw : ok_day wednesday :=
  okd_before wednesday thursday
    (okd_before thursday friday
       (okd_before friday saturday
          (okd_gd saturday gd_sat)
       db_sat)
    db_fri)
  db_thu.

コンストラクタをネストする。というのは何を意味しているのだろうか？