% The partial equivalence relation of the natural numbers.
eq_nat = lam2 [x][y] isNat x and eq x y.

% A "map" is an extensional relation from a per "eqt" to a per "equ"
% such that for every domain element there is a unique range element
% (modulo the pers).  It must map every element of the domain, and it
% must respect the equivalence relations.
map: tm (rel3 (per T) (per U) (rel T U)) =
  lam3 [eqt][equ][f]
   (forall4 [x][x'][y][y']
      eqt @ x @ x' imp f @ x @ y imp f @ x' @ y' imp equ @ y @ y')
   and (forall4 [x][x'][y][y']
         eqt @ x @ x' imp equ @ y @ y' imp
           (f @ x @ y equiv f @ x' @ y'))
   and (forall [x] eqt @ x @ x imp exists [y] f @ x @ y).

% Given two pers "eqt" and "equ", construct the per
% of relations from eqt to equ.
per_rel: tm (per T arrow per U arrow per (rel T U)) =
  lam4 [eqt][equ][f][g]
   forall4 [x][x'][y][y']
     eqt @ x @ x' imp equ @ y @ y' imp
     (f @ x @ y equiv g @ x' @ y').

% properties of the function f, with respect to eqt, phi, and a
rec_props: tm (per T) -> tm (rel T T) -> tm T -> tm (rel num T  arrow form) =
     [eqt][phi][a] lam [f] 
      map @ eq_nat @ eqt @ f   and 
      f @ zero @ a   and
      forall3 [n][x][x1]
         f @ succ n @ x1   imp   
         f @ n @ x  imp
         phi @ x @ x1.

per_exists_uniq: tm (per T) -> (tm T -> tm form) -> tm form =
  [eqt][f] exists [x] eqt @ x @ x and f x and forall [y] f y imp eqt @ x @ y.

rec_thm: pf (validper @ Eqt) ->
         pf (map @ Eqt @ Eqt @ Phi)  ->
         pf (Eqt @ A @ A) ->
         pf (per_exists_uniq (per_rel @ eq_nat @ Eqt) [f: tm (rel num T)] 
                 rec_props Eqt Phi A @ f) = 
 [p1][p2][p3]  cut p1 [_] cut p2 [_] cut p3 [_] bighole.