type nat = +{'zero : 1, 'succ : nat} type even = +{'zero : 1, 'succ : odd} type odd = +{ 'succ : even} type nat_cover = (even * odd) \/ (even * even) \/ (odd * odd) \/ (odd * even) comp ex1 : (nat * nat) -> <nat_cover> = fun x => <x> eval z: <nat> = <'zero ()> eval ex2 : <nat_cover> = let <x> = z in ex1 (x, x) type nat_cover_no_oo = (even * odd) \/ (even * even) \/ (odd * even) fail comp ex3 : (nat * nat) -> <nat_cover_no_oo> = fun x => <x>