- \lambda (k: K).(match k in K return (\lambda (k0: K).(\forall (i: nat).(eq
-nat (s k0 (r k0 i)) (S i)))) with [(Bind _) \Rightarrow (\lambda (i:
-nat).(refl_equal nat (S i))) | (Flat _) \Rightarrow (\lambda (i:
-nat).(refl_equal nat (S i)))]).
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(eq nat (s k0 (r k0
+i)) (S i)))) (\lambda (_: B).(\lambda (i: nat).(refl_equal nat (S i))))
+(\lambda (_: F).(\lambda (i: nat).(refl_equal nat (S i)))) k).