>#WIP
hstype family If (c :: Bool) t f type instance If 'True t f = t type instance If 'False t f = f
hstype family Add m n
hstype family Add m n :: Nat -> Nat -> Nat