一日寝てた。

台風が来てるなか、ぐーすか寝てた。
ベランダの鳩は健気にも強風のなかじっとしてた。でも抱卵の時期が長過ぎるような気がしないでもない。卵生きてんのか。

Inductive good_day : day -> Prop :=
 | gd_sat : good_day saturday
 | gd_sun : good_day sunday.

Inductive day_before : day -> day -> Prop :=
 | db_tue : day_before tuesday monday
 | db_wed : day_before wednesday tuesday
 | db_thu : day_before thursday wednesday
 | db_fri : day_before friday thursday
 | db_sat : day_before saturday friday
 | db_sun : day_before sunday saturday
 | db_mon : day_before monday sunday.

Inductive ok_day : day -> Prop :=
 | okd_gd : forall d:day,
    good_day d -> ok_day d
 | okd_before : forall d1 d2 : day,
    ok_day d2 -> day_before d2 d1 ->
    ok_day d1.

という定義があったとき、

okd_gd saturday gd_sat

がどーゆー構造というのか、どーゆー仕組みになっているとかがいまいっちょ分からん。
okd_gd saturday gd_sat
と
ok_day saturday
が同じであるということでよいのか？