type nat = +{'zero : 1, 'succ : nat} type even = +{'zero : 1, 'succ : odd} type odd = +{ 'succ : even} comp test1 : (nat - odd) -> <even> = fun x => <x> comp test2 : (nat - even) -> <odd> = fun x => <x> comp test3 : even -> <nat> = fun x => <x> (* cannot be even and odd at the same time => bottom *) comp test4 : (even /\ odd) -> <Bot> = fun x => <x> comp test5 : even -> <nat - odd> = fun x => <x> comp test6 : odd -> <nat - even> = fun x => <x>