Nuprl - Pf no_mention_implies_consistent

rho:Decl, t:Term, da:Collection(dec()), R:(LabelLabel). mentions_trace(t) trace_consistent(rho;da;R;t)

By: Auto THEN Unfold `trace_consistent` 0 THEN Analyze -3 THEN Easy

Generated subgoals:

None

About: