library S

spec S =

free type Bool ::= True | False

free type List ::= Nil | Cons(head :? Bool; tail :? List)

with Bool |-> bool, True |-> true', False |-> false',

List |-> list, Nil |-> nil, Cons |-> cons, head |-> Head,

tail |-> Tail

spec T =

free type bool ::= false' | true';

list ::= cons(Head :? bool; Tail :? list) | nil

view v : S to T