t:Type{i}, t':Type{j}, t'':Type{k}, c:t, c':t', c'':t''. case 3
: 3
c; 3
c'; 3 c''; 
t'' == inr(inr(
))
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_2] |
Try larger context:
ClassicalProps(jlc)