Nuprl - Pf decls_mng_rename

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

1. ds1: Collection(dec())
2. ds2: Collection(dec())
3. x: Label
4. y: Label
5. rho: Decl
6. v: [[d]] rho for d {d:dec()| d ds1 }(x)
7. d:dec(). d ds2 d.lbl = y mk_dec(x, d.typ) ds1

v [[d]] rho for d {d:dec()| d ds2 }(y)

By: All (Unfold `dall`) THEN All Reduce

Generated subgoal:

1 6. v: d:{d:dec()| d ds1 }. [[d]] rho(x)
7. d:dec(). d ds2 d.lbl = y mk_dec(x, d.typ) ds1
v (d:{d:dec()| d ds2 }. [[d]] rho(y))

About:

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