WhoCites Definitions MarkB generic Sections NuprlLIB Doc

Who Cites iseg?
isegDef l1 l2 == l:T List. l2 = (l1 @ l)
Thm* T:Type, l1,l2:T List. l1 l2 Prop
append Def as @ bs == Case of as; nil bs ; a.as' [a / (as' @ bs)] (recursive)
Thm* T:Type, as,bs:T List. (as @ bs) T List

Syntax:l1 l2 has structure: iseg(T; l1; l2)

About:
listconslist_ind
recursive_def_noticeuniverseequalmemberpropallexists
!abstraction

WhoCites Definitions MarkB generic Sections NuprlLIB Doc