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 == inr(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_1] |
| Thm* 3 = 3 | [Three_eq_contradiction_ext] |
Try larger context:
ClassicalProps(jlc)