Nuprl - Pf trace consistent action pre 1 1

1. A: ioa{i:l}()
2. rho: Decl
3. te: LabelLabel
4. k: Label
5. r: rel()
6. r action_pre(k;A.pre)
7. rel_mentions_trace(r)

p:pre(). p A.pre & rel_mentions_trace(p.rel)

By: Unfold `action_pre` -2 THEN RW ColMemberC -2 THEN ExRepD THEN InstConcl [p] THEN SubstFor p.rel 0

Generated subgoals:

None

About: