On fixed points in (full classical) linear logic

Proposition [Least and greatest fixed point in LL]

For any formula A(x) \in LL where x occurs positively, then

/\ x.(!(A(x) -0 x) -0 x)

is the least fixed point in (full classical) LL ordered by |- of 
the mapping x |-> A(x).
Greatest fixed point is (indeed) dual.

My questions are then~:
	1. Is that already known ? (or (nobody is perfect) false ??) 
        (I can post the proof if this is new...)
        2. Is there any (non trivial) statement of unicity of such
	least (and greatest) fixed points ?
        3. I have already made some (draft) works towards the 
        specification of processes within LL (quite straigforwardly
        encoding (syntactic) CCS like processes as formulae in LL
        with phase semantics seen as a testing semantics) and such
        fixed  point constructors enable  me to describe as LL
        formulae  specification of infinite (regular) behaviours. 
        Is there any recent work in that direction ?
Thanks for any comments,
David Janin
LaBRI - Universite' de Bordeaux | janin@labri.u-bordeaux.fr 
351, cours de la Liberation     | Tel : (33) 56 84 69 12 
33 405 Talence FRANCE           | Fax : (33) 56 84 66 69