some news on predicate logic

Hi!

I finally managed to write up: 

1)  an internal deep inference cut elimination procedure for predicate logic: 
http://www.iam.unibe.ch/~kai/Current/q.pdf , and

2) a translation between deep inference and two-sided sequent
calculus, which gives us a clue on what a "normal" deep inference
derivation should be:
http://www.iam.unibe.ch/~kai/Current/n.pdf .

I'm eagerly awaiting your comments!

-Kai