IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
multiply functionality wrt assoced11 1. a : 2. a' : 3. b : 4. b' : 5. c1 : 6. a' = ac1 7. a' | a 8. c : 9. b' = bc 10. b' | b ab | a'b'
By:
Witness cc1 THEN (HypSubst 6 0) THEN (HypSubst 9 0)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html