recursion - 平等の教会符号化のための再帰

Question

N正の整数の Church エンコーディングでは、再帰原理を定義できnat_recます。

Definition N : Type :=
forall (X:Type), X->(X->X)->X.

Definition nat_rec (z:N)(s:N->N)(n:N) : N :=
n N z s.

次の教会の平等のequal_recコード化の再帰原則は何ですか?equal

Definition equal (x:A) : A->Type :=
fun x' => forall (P:A->Type), P x -> P x'.

Definition equal_rec (* ... *)