class Type < Type

var t : Type

class TYPE < Type

type Pred __ : -Type -> Type;

Unit : TYPE

class a, b, c < Type

class 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