Nuprl - Pf rel arg typ wf

r:rel(), de:sig(), i:. tc1(r;de) i < ||r.args|| rel_arg_typ(r.name;i;de) SimpleType

By: Analyze 0 THEN Unfolds [`tc1`;`rel_arg_typ`] 0 THEN Analyze 1 THEN Analyze 1 THEN All Reduce

Generated subgoals:

None

About: