Nuprl - Pf term mng tappend 1

(3steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

1. u: Term
2. u1: TermType{i'}
3. w: u:{v:Term| u1(v) }d:Decl{i}, tr:trace_env(d), a:(d), e,s,v:Top. affects_trace(tr.proj;kind(a);u) ([[u]] e s v tappend(tr;a) ~ [[u]] e s v tr)
4. y1: Label

d:Decl{i}, tr:trace_env(d), a:(d), e,s,v:Top. tr.proj(y1,kind(a)) (tappend(tr;a).y1 ~ tr.y1)

By: UnivCD THEN Unfolds [`tappend`;`tproj`] 0 THEN Reduce 0 THEN SplitOnConclITE THEN Easy

Generated subgoals:

None

About:

(3steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc