Who Cites tappend?
tappend	Def tappend(tr;a) == mk_trace_env(tr.trace @ [a], tr.proj)
	Thm* d:Decl, tr:trace_env(d), a:(d). tappend(tr;a) trace_env(d)
trace_env_proj	Def t.proj == 2of(t)
	Thm* d:Decl, t:trace_env(d). t.proj LabelLabel
trace_env_trace	Def t.trace == 1of(t)
	Thm* d:Decl, t:trace_env(d). t.trace (d) 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
mk_trace_env	Def mk_trace_env(trace, proj) == < trace,proj >
	Thm* d:Decl, trace:(d) List, proj:(LabelLabel). mk_trace_env(trace, proj) trace_env(d)
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A

Syntax:

tappend(tr;a)

has structure:

tappend(tr; a)

About: