IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hlength eq cons
'a:S.
all
(
P:hlist('a)
(
hbool. all
( hbool. (n:hnum. equal
( hbool. (n:hnum. (all
( hbool. (n:hnum. ((l:hlist('a). implies(equal(length(l),suc(n)),P(l)))
( hbool. (n:hnum. ,all
( hbool. (n:hnum. ,(l:hlist('a). implies
( hbool. (n:hnum. ,(l:hlist('a). (equal(length(l),n)
( hbool. (n:hnum. ,(l:hlist('a). ,(l:hlist('a). all
( hbool. (n:hnum. ,(l:hlist('a). ,(l:hlist('a). (x:'a. P(cons(x,l))))
( hbool. (n:hnum. ,(l:hlist('a). ,(l))))))
| By: |
HOL "hlength_eq_cons" |
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
