Nuprl - Proof: multiply functionality wrt assoced 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: multiply functionality wrt assoced 2 1

1. a :

2. a' :

3. b :

4. b' :

5. a | a'
6. c1 :

7. a = a'

c1
8. b | b'
9. c :

10. b = b'

b' | a

By:	Witness cc1 THEN (HypSubst 7 0) THEN (HypSubst 10 0)

Generated subgoals:

None

About:

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