SKK とか

K I = F と、S K K = I を証明してみる。

Definition I {A:Type} x:A := x.
Definition K {A B:Type} (x:A) (y:B) := x.
Definition F {A B:Type} (x:A) (y:B) := y.
Definition S {A B C:Type} (x:A->B->C) (y:A->B) (z:A) := x z (y z).

Theorem ki_f : forall (A B:Type)(x:A)(y:B), K I x y = F x y.
Proof.
  intros A B x y.
  unfold K.
  unfold I.
  unfold F.
  reflexivity.
Qed.

Theorem skk_i : forall (A B:Type)(x:A), S K (K:A->B->A) x = I x.
Proof.
  intros A B x.
  unfold S.
  unfold K.
  unfold I.
  reflexivity.
Qed.

まぁ、展開するだけなんですけどね。