Nuprl - Pf tc pred pred rel

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 Auto'' THEN HypSubstSq -1 0 THEN Trivial

Generated subgoals:

None

About: