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