Definitions graph 1 1 Sections Graphs Doc

Some definitions of interest.
l_member Def (x l) == i:. i < ||l|| & x = l[i] T
Thm* T:Type, x:T, l:T List. (x l) Prop
rev_implies Def P Q == Q P
Thm* A,B:Prop. (A B) Prop
reverse Def rev(as) == Case of as; nil nil ; a.as' rev(as') @ [a] (recursive)
Thm* T:Type, as:T List. rev(as) T List

About:
listconsnillist_indless_than
recursive_def_noticeuniverseequalmemberpropimpliesallexists
!abstraction

Definitions graph 1 1 Sections Graphs Doc