IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eq cons imp eq hds122 1. A : Type
2. a : A 3. b : A 4. as : A List
5. bs : A List
6. a.as = b.bs 7. a.as = b.bs 8. hd((a.as)) = hd((b.bs))
a = b
By:
Reduce 8
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
a = b
