(2steps total) PrintForm Definitions Lemmas core StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sq stable iff 1
1. P : Prop
2. Q : Prop
3. SqStable(P)
4. SqStable(Q)
  SqStable(P  Q)
By: Repeat (Unfolds [`iff`;`rev_implies`] 0)
THEN
Backchain
[Thm* SqStable(P)  SqStable(Q)  SqStable(P & Q)
;Thm* SqStable(Q)  SqStable(P  Q)]

Generated subgoals:

None

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

(2steps total) PrintForm Definitions Lemmas core StandardLIB Doc