1 2 3 4 5 6 7 8
Type (fun x : nat => match x return nat with | S x as b => match x with | x => x end end).