class Type

var t:Type

class TYPE : {x.x < t}

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

class a, b, c

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

%[% [ ] % %[

]%

%[ ]%

]%

%[ ]%

sort s

op a: (?s); %[ Should be: op a:?s ]%

type Data1 ::= a | b | c;

type Data2 ::= Cons21 (Data1; Data2) | Cons22(Data2; Data1) | sort 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)?

axioms true ;forall x:s.e;

forall x:s.e