class Type

var t : Type

class TYPE

types Pred __ : -Type -> Type;

Unit : TYPE

classes a, b, c

classes a, b, c < d;

a < b

type s : c

pred tt : s

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;

pred eq : s * s

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;