Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
t:
.
t':
{j}.
t'':
{k}.
c:t.
c':t'.
c'':t''. case 3
: 3
c'; 3
c''; 3
c;
t''
Applied Tactic:
AbReduce 0 THEN Auto
Generated subgoals:
None
t:
. t':{j}. t'':{k}. c:t. c':t'. c'':t''. case 3
: 3
c'; 3 c''; 3
c; 
t''