is mentioned by

Thm* x,y:. Dec(x = y)	[decidable__equal_Three]
Thm* t:Type{i}, t':Type{j}, t'':Type{k}, c:t, c':t', c'':t''. case 3: 3 c; 3 c'; 3 c''; t''	[Three_case_wf_2]
Thm* t:Type{i}, t':Type{j}, t'':Type{k}, c:t, c':t', c'':t''. case 3: 3 c'; 3 c''; 3 c; t''	[Three_case_wf_1]
Thm* t:Type{i}, t':Type{j}, t'':Type{k}, c:t, c':t', c'':t''. case 3: 3 c; 3 c'; 3 c''; t	[Three_case_wf_0]
Thm* x:. True	[Three_ind_ext]

In prior sections: core fun 1 well fnd int 1 bool 1 union rel 1 quot 1 sqequal 1 prog 1 int 2 list 1 lambda jlc bool 2 jlc discrete jlc core 3 jlc list 3 jlc

Try larger context: ClassicalProps(jlc)