Who Cites tc1?
tc1	Def tc1(r;de) == Case(r.name) Case eq(Q) = > ||r.args|| = 2 Case R = > ||de.rel(R)|| = ||r.args|| Default = > False
case_default	Def Default = > body(value,value) == body
rel_args	Def t.args == 2of(t)
length	Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)
	Thm* A:Type, l:A List. ||l||
	Thm* ||nil||
sig_rel	Def t.rel == 2of(t)
nat	Def == {i:| 0i }
	Thm* Type
case_relname_other	Def Case x = > body(x) cont(x1,z) == (x1.inr(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x1])
case_relname_eq	Def Case eq(x) = > body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z))
rel_name	Def t.name == 1of(t)
case	Def Case(value) body == body(value,value)
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))
le	Def AB == B < A
	Thm* i,j:. (ij) Prop
hd	Def hd(l) == Case of l; nil "?" ; h.t h
	Thm* A:Type, l:A List. ||l||1 hd(l) A
	Thm* A:Type, l:A List. hd(l) A
tl	Def tl(l) == Case of l; nil nil ; h.t t
	Thm* A:Type, l:A List. tl(l) A List
case_inr	Def inr(x) = > body(x) cont(value,contvalue) == InjCase(value; _. cont(contvalue,contvalue); x. body(x))
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A
not	Def A == A False
	Thm* A:Prop. (A) Prop

Syntax:

tc1(r;de)

has structure:

tc1(r; de)

About: