Definitions graph 1 1 Sections Graphs Doc

Some definitions of interest.
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
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
iff Def P Q == (P Q) & (P Q)
Thm* A,B:Prop. (A B) Prop
l_disjoint Def l_disjoint(T;l1;l2) == x:T. ((x l1) & (x l2))
Thm* T:Type, l,l':T List. l_disjoint(T;l;l') Prop
l_member Def (x l) == i:. i < ||l|| & x = l[i] T
Thm* T:Type, x:T, l:T List. (x l) Prop
no_repeats Def no_repeats(T;l) == i,j:. i < ||l|| j < ||l|| i = j l[i] = l[j] T
Thm* T:Type, l:T List. no_repeats(T;l) Prop
not Def A == A False
Thm* A:Prop. (A) Prop

About:
listconsconsnil
list_indless_than
recursive_def_noticeuniverseequalmemberpropimpliesand
falseallexists!abstraction

Definitions graph 1 1 Sections Graphs Doc