map_i: ...
map_e: ...

per_rel_i: ...
per_rel_e: ...

% symmetric  is defined in core/rel/eq.elf
% Some useful lemmas  per_refl, per_symm, per_trans are in core/per/per.elf.

symmetric_i: ({x}{y} pf (R @ x @ y) -> pf (R @ y @ x)) -> 
               pf (symmetric @ R) = ...
transitive_i: ...

symmetric_per_rel: pf (validper @ Eqt) -> pf (validper @ Equ) ->
              pf (symmetric @ (per_rel @ Eqt @ Equ)) = ...

transitive_per_rel: ...
validper_per_rel: pf (validper @ Eqt) -> pf (validper @ Equ) ->
              pf (validper @ (per_rel @ Eqt @ Equ)) =


% This is the \Gamma from Jacobson's proof:  (gamma Eqt Phi A) is the
% set of all relations U such that U(0,A) and if (n,b)\in U then 
%  (n+,Phi(b))\in U.
gamma: tm (per T) -> tm (rel T T) -> tm T -> tm (set (rel num T)) = ...

gamma = [eqt][phi][a] lam [u] u @ zero @ a  and  ..


gamma_e1: pf (gamma Eqt Phi A @ U) -> pf (per_rel @ eq_nat @ Eqt @ U @ U) =
  ...
gamma_e2: ...
gamma_e3: ...

% This is the intersection of all the relations in \Gamma
intgamma: tm (per T) -> tm (rel T T) -> tm T -> tm (rel num T) =

intgamma_i: ...
intgamma_e: 

per_exists_uniq_i: ...
per_exists_uniq_e: ...
                   
% The definition of validper can be found in core/per/per.elf; first
% prove lemmas symmetric @ eq_nat   and   transitive @ eq_nat.
validper_eq_nat: pf (validper @ eq_nat) = bighole.

validper_per_rel: pf (validper @ Eqt) -> pf (validper @ Equ) ->
                   pf (validper @ (per_rel @ Eqt @ Equ)) =
 [p1][p2] cut p1 [_] cut p2 [_] bighole.

map_per_rel: pf (validper @ Eqt) ->
     pf (per_rel @ eq_nat @ Eqt @ intgamma Eqt Phi A @ intgamma Eqt Phi A) =
 [p0: pf (validper @ Eqt)] 
 cut p0 [_]
 bighole.

% As Jacobson says, "Since N \times S has these properties it is
% clear that \Gamma \not= \emptyset.
gamma_nonempty: pf (validper @ Eqt) ->
		pf (map @ Eqt @ Eqt @ Phi)  ->
                pf (Eqt @ A @ A) ->
               pf (exists [u] gamma Eqt Phi A @ u) =
 [p0: pf (validper @ Eqt)]
 [p1: pf (map @ Eqt @ Eqt @ Phi)]
 [p2: pf (Eqt @ A @ A)]
 cut p0 [_] cut p1 [_] cut p2 [_] bighole.

% This induction hypothesis is almost right, but not quite.
% I believe the problem is that the first conjunct
%  (map @ eq_nat @ eqt @ intgamma eqt phi a)  
% must itself be proved by induction over k.
% Try and prove the base case (i.e., rec_props_base) 
% and see what happens.  We'll discuss in class how to adjust
% the hypothesis.
rec_props_hyp: 
     tm (per T) -> tm (rel T T) -> tm T -> 
          tm num -> tm form =
     [eqt][phi][a][k]
      map @ eq_nat @ eqt @ intgamma eqt phi a   and 
      intgamma eqt phi a @ zero @ a   and
      forall3 [n][x][x1]
         inrange @ k @ n imp 
         intgamma eqt phi a @ succ n @ x1   imp   
         intgamma eqt phi a @ n @ x  imp
         phi @ x @ x1.

rec_props_base: 
         pf (validper @ Eqt) ->
         pf (map @ Eqt @ Eqt @ Phi)  ->
         pf (Eqt @ A @ A) ->
         pf (rec_props_hyp Eqt Phi A  zero) = ...
 
rec_props_step: 
         pf (validper @ Eqt) ->
         pf (map @ Eqt @ Eqt @ Phi)  ->
         pf (Eqt @ A @ A) ->
         {K} pf (isNat K) ->
         pf (rec_props_hyp Eqt Phi A K) ->
         pf (rec_props_hyp Eqt Phi A (succ K)) = ...