Nuprl - Pf decls_mng

(5steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

ds1,ds2:Collection(dec()), rho:Decl, r:{[[ds1]] rho}. ds2 ds1 r {[[ds2]] rho}

By: Unfold `record` 0 THEN Unfold `decl_type` 0 THEN Try (Fold `decl` 0)

Generated subgoal:

1 1. ds1: Collection(dec())
2. ds2: Collection(dec())
3. rho: Decl
4. r: l:Label[[ds1]] rho(l)
5. ds2 ds1
6. x1: Label
([[ds1]] rho(x1)) ([[ds2]] rho(x1))

About:

(5steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc