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 ?
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 ?