At:
tc pred col all p:Collection(rel()), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc_pred(p;ds;da;de) (rp.tc(r;ds;da;de))
By:
(UnivCD THEN (RWW "col_all_iff" 0)) THENA (Auto THEN (Try (Unfold `pred` 0)))
THEN
Unfold `tc_pred` 0
THEN
RelRST
Generated subgoals:
p:Collection(rel()), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc_pred(p;ds;da;de) 
(
p.tc(r;ds;da;de))