Re: Term syntax for derivations in Deep-Inference systems

Steven Lengrand wrote:

> Hello,
>  
> I have written a short note


Me too, me too!

It's at http://www.iam.unibe.ch/~kai/Current/prty.pdf and it's along the 
same lines as Stephane's term calculus with the minor twist that I 
identify proofs and types. This allows to capture formalism B.

It could also be just wrong. (unsound, inconsistent, illegal...) So I'm 
also interested in comments. Could you please check, Stephane? Alessio, 
could you check whether you agree that this formalism B?

-Kai