Nuprl - Pf trace consistent pred unprime 1 1

da:Collection(dec()), rho:Decl, te:(LabelLabel), t:Term. trace_consistent(rho;da;te;t) trace_consistent(rho;da;te;unprime(t))

By: Auto THEN RepeatFor 3 (ParallelOp -1) THEN Lemmaize [-1]

Generated subgoal:

1 t:Term, g:Label. term_mentions_guard(g;unprime(t)) term_mentions_guard(g;t)

About: