Nuprl - Pf trace consistent pred unprime 1 1 1

(4steps) PrintForm Definitions mb automata 4 Sections GenAutomata Doc

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

By: Auto THEN MoveToConcl -1 THEN Unfold `unprime` 0 THEN TermInd 1 THEN All Reduce THEN AllHyps (Fold `unprime`) THEN All (RW assert_pushdownC) THEN ParallelOp -1 THEN EasyHyp

Generated subgoals:

None

About:

(4steps) PrintForm Definitions mb automata 4 Sections GenAutomata Doc