pal

Software Foundation Prop.v

forall l, l = rev l -> pal l.

どっから手をつけたらいいかすら分からん・・・

前問の

forall l, pal l -> l = rev l.

ならば、"pal l"という命題を定義してあるから、そのコンストラクタに応じて場合わけして、それぞれが l = rev lを満たすことを示して、とゆう感じで分からんでもない。

l = rev lっていきなり出されても。
lに関する帰納法をやっても,そもそも全てのlが l = rev lを満たす訳ないし、
l = rev lという命題は定義されてないし、

どうすりゃいいの？

• -

pal lを定義したように、 l = rev lを定義すりゃいいのかしら。
オレオレ定義してよいものなのか。しかし、 XX = YY という形の命題をどうやって生成定義すればいいのかわからん。