Definitions graph 1 1 Sections Graphs Doc

Some definitions of interest.
assert Def b == if b True else False fi
Thm* b:. b Prop
mapoutl Def mapoutl(s) == mapfilter(x.outl(x);x.isl(x);s)
Thm* A,B:Type, s:(A+B) List. mapoutl(s) A List
isl Def isl(x) == InjCase(x; y. true; z. false)
Thm* A,B:Type, x:A+B. isl(x)
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
outl Def outl(x) == InjCase(x; y. y; z. "???")
Thm* A,B:Type, x:A+B. isl(x) outl(x) A

About:
listboolbfalsebtrueifthenelseassertless_thantoken
uniondecidelambdauniverseequalmember
propimpliesfalsetrueallexists!abstraction

Definitions graph 1 1 Sections Graphs Doc