IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
heq list 'a:S.
all
(h1:'a. all
(h1:'a. (h2:'a. implies
(h1:'a. (h2:'a. (equal(h1,h2)
(h1:'a. (h2:'a. ,all
(h1:'a. (h2:'a. ,(l1:hlist('a). all
(h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). implies
(h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). (equal(l1,l2)
(h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ,equal
(h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ,(cons(h1,l1)
(h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ,,cons(h2,l2))))))))
By:
HOL "heq_list"
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
'a:S.
all
h1:'a. all
