Nuprl - Pf trace consistent pred wf

p:Fmla, rho:Decl, da:Collection(dec()), R:(LabelLabel). trace_consistent_pred(rho;da;R;p) Prop

By: Unfold `trace_consistent_pred` 0 THEN Fold `pred` 0

Generated subgoals:

None

About: