Nuprl - Pf tc

At: tc wf

r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) Prop

By: Unfolds [`rel`;`tc`] 0 THEN UnivCD THEN Analyze 1 THEN Analyze 1 THEN Reduce 0

Generated subgoals:

None

About: