IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
mapcons wf12 1. A : Type
2. B : Type
3. f : A(A List)B 4. A List
5. u : A 6. v : A List
7. mapcons(f;v) B List
f(u,v).mapcons(f;v) B List
By:
MemberEqCD
Generated subgoals:
1
f(u,v) B
Auto
2
mapcons(f;v) B List
Hypothesis
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html