Thorsten Altenkirch wrote:
Just for the record: I suggested to show: f : Fin (suc m) -> Fin (suc n); Injective f ------------------------------------------------------------ restrict f : (f' : Fin m -> Fin n; Injective f') in freely invented syntax.
Quite. And Gutman is currently checking what I allege to be a proof of some such. I am currently checking a gin and tonic.
Night all Conor This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.
