i:Id, A,B:MsgA. @i: A  @i: B  A  B

By:	UnivCD THEN Repeat (Unfolds [`d-sub`;`s-dsys`;`m-sys-at`;`d-m`] 0 THEN Reduce 0) THENL [InstHyp [i] -1;SplitOnConclITE] THEN Try (BackThru Thm* M1,M2:MsgA. M1 = M2  M1  M2 THEN Complete Auto)

1

1. i : Id 2. A : MsgA 3. B : MsgA 4. i@0:Id. if i@0 = i A else  fi  if i@0 = i B else  fi 5. if i = i A else  fi  if i = i B else  fi   A  B

1 step

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html