rel (A:Set) = (x:A,y:A) -> Set : Type,

pred (A:Set) = (x:A) -> Set : Type,

inclusPred (A:Set,P:pred A,Q:pred A) =
  (x:A,h:P x) -> Q x : Set,

ref (A:Set,R:rel A) = (x:A) -> R x x : Set,

trans (A:Set,R:rel A) = (x:A,y:A,z:A,h1:R x y,h2:R y z) -> R x z 
              : Set,

and (A:Set,B:Set) = sig {fst:A,snd:B} : Set,

exists (A:Set,B:pred A) = sig {fst:A,snd:B fst} : Set,

{- we build a positivity predicate -}

N = data {$0,$S (x:N)} : Set,

succ (n:N) = $S n : N,

zero = $0 : N,

one = succ zero : N,

N1 = data {$0} : Set,

N0 = data {} : Set,

elimN0 (x:N0,A:Set) = case x of {} : A,

fun (A:Set,B:Set) = (x:A)->B : Set,

subset (A:Set) = sig {I:Set,f:fun I A} : Type,

inclus (A:Set,leq:rel A,s:subset A,t:subset A) =
 (i:s.I) -> exists (t.I) (\ j -> leq (s.f i) (t.f j))
  : Set,

make_subset (A:Set,I:Set,f:fun I A) =
 struct {I = I,f = f} : subset A,

theory_pos (A:Set,B:pred A,C:(x:A,y:B x)->Set,
            f:(x:A,e:B x,r:C x e) -> A,
            leq:rel A,is_trans:trans A leq,is_ref:ref A leq,
            loc:(x:A,y:A,h1:leq y x,e:B x) ->
                exists (B y) 
                       (\ e1 -> inclus A leq 
                                       (make_subset A (C y e1) (f y e1))
                                       (make_subset A (C x e) (f x e))))
 = theory 
    {S (n:N,x:A) = 
       case n of
         {$0 -> N1,
          $S n1 -> 
            (e:B x) -> exists (C x e) (\ r -> S n1 (f x e r))
         } : Set,
     D (n:N) = exists A (S n) : Set,
     makeD (n:N,a:A,s:S n a) = struct {fst = a,snd = s} : D n,
     mapD (n:N,x:A,e:B x,s:S (succ n) x) =
       let {r = (s e).fst : C x e,
            t = (s e).snd : S n (f x e r)}
       in makeD n (f x e r) t : D n,
     leqD (n:N,v:D (succ n),u:D n) =
        case n of
          {$0 -> leq (v.fst) (u.fst),
           $S n1 -> let {b = v.fst : A,
                         a = u.fst : A,
                         t = v.snd : S (succ n) b,
                         s = u.snd : S n a}
                    in and (leq b a)
                           ((e:B a) -> exists (B b) 
                                              (\ e1 -> leqD n1 (mapD n b e1 t) (mapD n1 a e s)))}
         : Set,
     lem1 (n:N,v:D (succ n),u:D n,p:leqD n v u) =
        case n of
           {$0 -> p,
            $S n1 -> p.fst}
         : leq (v.fst) (u.fst),
     pos = \ a -> exists ((n:N) -> D n)
                         (\ d -> and (leq ((d zero).fst) a)
                                     ((n:N) -> leqD n (d (succ n)) (d n)))
         : pred A,

    lem2 (a:A,p:pos a,e:B a) = 
        let {fp = p.fst : (n:N) -> D n,
             gp = \ n -> (fp n).fst : fun N A,
             hp = \ n -> (fp n).snd : (n:N) -> S n (gp n),
             a0 = gp zero : A,
             a1 = gp one : A,
             rem1 = p.snd.fst : leq a0 a,
             rem2 = p.snd.snd : (n:N) -> leqD n (fp (succ n)) (fp n),
             rem3 (n:N) = lem1 n (fp (succ n)) (fp n) (rem2 n) 
                        : leq (gp (succ n)) (gp n),
             rem4 = is_trans a1 a0 a (rem3 zero) rem1 : leq a1 a,
             e1 = (loc a a1 rem4 e).fst : B a1,
             I = C a e : Set,
             I1 = C a1 e1 : Set,
             g = f a e : fun I A,
             g1 = f a1 e1 : fun I1 A,
             sub = make_subset A I g : subset A,
             sub1 = make_subset A I1 g1 : subset A,
             rem5 = (loc a a1 rem4 e).snd : inclus A leq sub1 sub,
             st1 = hp one : S one a1,
             r1 = (st1 e1).fst : I1,
             b1 = f a1 e1 r1 : A,
             r = (rem5 r1).fst : I,
             b = f a e r : A,
             rem6 = (rem5 r1).snd : leq b1 b,
             es (n:N) = 
               case n of
                {$0 -> e1,
                 $S n1 -> let {en1 = es n1 : B (gp n),
                               rem7 = rem2 n : leqD n (fp (succ n)) (fp n)}
                          in (rem7.snd en1).fst
                }
                : B (gp (succ n)),
            fq (n:N) = mapD n (gp (succ n)) (es n) (hp (succ n)) : D n,
            rem7 (n:N) = ((rem2 (succ n)).snd (es n)).snd
                : leqD n (fq (succ n)) (fq n)
            }
        in struct {fst = r,
                   snd = struct {fst = fq,
                                 snd = struct {fst = rem6,
                                               snd = rem7}}}
         : exists (C a e) (\ r -> pos (f a e r)),

     head (a:A,b:B a,p:pos a) = (lem2 a p b).fst : C a b,

     tail (a:A,b:B a,p:pos a) = (lem2 a p b).snd : pos (f a b (head a b p)),

     productive (X:pred A) = 
       (a:A,p:X a,e:B a) -> exists (C a e) (\ r -> X (f a e r))
         : Set,


     isProductive (X:pred A,
                   h:(a:A,e:B a,p:X a) -> (C a e),
                   g:(a:A,e:B a,p:X a) -> X (f a e (h a e p))) =
     \ a p e -> struct {fst = h a e p,snd = g a e p} : productive X,

     lem3 (X:pred A,h:productive X) = 
       let {sX (n:N,a:A,p:X a) =
             case n of
              {$0 -> $0,
               $S n1 -> let {r (e:B a) = (h a p e).fst : C a e,
                             next (e:B a) = f a e (r e) : A,
                             q (e:B a) = (h a p e).snd : X (next e)}
                        in \ e -> struct {fst = r e,snd = sX n1 (next e) (q e)}}
               : S n a,
            dX (a:A,p:X a,n:N) = makeD n a (sX n a p) : D n,
            rem1 (a:A,p:X a,n:N) = 
             case n of
              {$0 -> is_ref a,
               $S n1 -> struct {fst = is_ref a,
                                snd = \ e -> struct {fst = e,
                                                     snd = rem1 (f a e ((h a p e).fst)) ((h a p e).snd) n1}}
              }
               : leqD n (dX a p (succ n)) (dX a p n),
            rem2 (a:A,p:X a) = is_ref a : leq ((dX a p zero).fst) a
           }
       in \ a p -> struct {fst = dX a p,
                           snd = struct {fst = rem2 a p,
                                         snd = rem1 a p}}
         : (a:A,p:X a) -> pos a,

     Elim (X:pred A,
           h:(a:A,e:B a,p:X a) -> (C a e),
           g:(a:A,e:B a,p:X a) -> X (f a e (h a e p)),
           a:A,
           p:X a) =
     lem3 X (isProductive X h g) a p : pos a,

     thm1 = lem2 : productive pos,
     thm2 (X:pred A,h:productive X) = lem3 X h : inclusPred A X pos
    } : Theory