IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
is list mem wf121 1. A : Type
2. a : A 3. A List
4. u : A 5. v : A List
6. (av) Prop
(a = u (av)) Prop
By:
Analyze
Generated subgoals:
1
(a = u) Prop
Auto
2
(av) Prop
Hypothesis
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html