IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
iseg map1 1. A : Type
2. B : Type
3. f : AB 4. L1 : A List
5. L2 : A List
6. l : A List
7. L2 = (L1 @ l)
l@0:B List. map(f;L1 @ l) = (map(f;L1) @ l@0)
By:
RW MapAppendC 0 THEN InstConcl [map(f;l)]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
B
l@0:B List. map(f;L1 @ l) = (map(f;L1) @ l@0)
