t:Type{i}, t':Type{j}, t'':Type{k}, c:t, c':t', c'':t''. case 3
: 3 
c; 3
c'; 3
c''; 
t
3 = 3 == inl(
)
is mentioned by
| 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* 3 = 3 | [Three_eq_contradiction_ext] |
Try larger context:
ClassicalProps(jlc)