At:
tc pred singleton
r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc_pred( < r > ;ds;da;de) 
tc(r;ds;da;de)
By:
Unfolds [`tc_pred`;`pred_rel`] 0
THEN
RW ColMemberC 0
THEN
Try BackThruSomeHyp
THEN
TrivialSubst
Generated subgoals:
None
About:
