class Type < Type

var t : Type

class TYPE < {x . x < t}

type Pred __ : Type- -> Type; Unit : TYPE

class a, b, c < Type

class a, b, c < d; a < b

type s : c

predfun tt : s ->? Unit

var x : s

program tt = \ x : s . ()

program __ res __ (x : s, y : t) : s = x;

fst (x : s, y : t) : s = x; snd (x : s, y : t) : t = y

predfun eq : s � s ->? Unit

type s < ? s

program all (p : (? s)) : (? Unit) = eq (p, tt)

program And (x, y : (? Unit)) : (? Unit) = t1 () res t2 ()

program __ impl __ (x, y : (? Unit)) = eq (x, x And y)

program __ or __ (x, y : (? Unit)) : (? Unit) =

all (\ r : (? Unit) . ((x impl r) res (y impl r)) impl r);

ex (p : (? s)) : (? Unit) =

all (\ r : (? Unit) . all (\ x : s . p (x) impl r) impl r);

ff () : (? Unit) = all (\ r : (? Unit) . r ())

forall x : t; y : t

. %(..)%

x = y

type s

op a : (? s)

type Data1 ::= a |

b |

c

type Data2 ::= Cons21 (Data1; Data2) |

Cons22 (Data2; Data1) |

type Data1

type Data3 ::= Cons31 (sel1:? Data1; sel2:? Data2) |

Cons32 (sel2:? Data2; sel1:? Data1)

type Data4 ::= Cons41 (sel1:? Data1; sel2:? Data2) ? |

Cons42 (sel2:? Data2; sel1:? Data1) ?

. true

forall x : s

. e

forall x : s

. e