i,a,x:Id, A,T:Type, c:A, P:(ATProp).
  @i: ma-single-pre-init1(x;A;c;a;T;x,v.P(x,v))  Dsys
  & (D:Dsys. 
  & (@i: ma-single-pre-init1(x;A;c;a;T;x,v.P(x,v))  D
  & (
  & (D 
  & (realizes es.(vartype(i;x) r A)
  & (realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A)
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id
  & (realizes es.& (
  & (realizes es.& (kind(e) = locl(a)  Knd  (valtype(e) r T))
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id
  & (realizes es.& (
  & (realizes es.& (kind(e) = locl(a)  Knd  P((x when e),val(e)))
  & (realizes es.& & ((v:T. P(c,v))
  & (realizes es.& & (
  & (realizes es.& & ((e:E. 
  & (realizes es.& & ((loc(e) = i  Id
  & (realizes es.& & ((& kind(e) = locl(a)  Knd  (v:T. P((x after e),v)))))

By:	Unfold `ma-single-pre-init1` 0 THEN UnivCD THEN Assert ((s,v. P(s(x),v))  State(x : A)TProp)

1	1. Id 2. Id 3. x : Id 4. A : Type 5. T : Type 6. A 7. P : ATProp   (s,v. P(s(x),v))  State(x : A)TProp	7 steps
2	1. i : Id 2. a : Id 3. x : Id 4. A : Type 5. T : Type 6. c : A 7. P : ATProp 8. (s,v. P(s(x),v))  State(x : A)TProp   @i: (with ds: x : A   @init: x : c   action a:T   aprecondition a(v) is   as,v. P(s(x),v))    Dsys   & (D:Dsys.    & (@i: (with ds: x : A   & (@init: x : c   & (action a:T   & (aprecondition a(v) is   & (as,v. P(s(x),v))  D   & (   & (D    & (realizes es.(vartype(i;x) r A)   & (realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A)   & (realizes es.& (e:E.    & (realizes es.& (loc(e) = i  Id   & (realizes es.& (   & (realizes es.& (kind(e) = locl(a)  Knd  (valtype(e) r T))   & (realizes es.& (e:E.    & (realizes es.& (loc(e) = i  Id   & (realizes es.& (   & (realizes es.& (kind(e) = locl(a)  Knd  P((x when e),val(e)))   & (realizes es.& & ((v:T. P(c,v))   & (realizes es.& & (   & (realizes es.& & ((e:E.    & (realizes es.& & ((loc(e) = i  Id   & (realizes es.& & ((& kind(e) = locl(a)  Knd  (v:T. P((x after e),v)))))	35 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html