Nuprl - Pf decls_mng_functionality 1 1

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

1. ds1: Collection(dec())
2. ds2: Collection(dec())
3. rho: Decl
4. r: l:Labeldecl_type([[ds1]] rho;l)
5. ds1 = ds2
6. x1: Label
7. x: decl_type([[ds1]] rho;x1)

x decl_type([[ds2]] rho;x1)

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

Generated subgoal:

1 4. r: l:Label[[ds1]] rho(l)
5. ds1 = ds2
6. x1: Label
7. x: [[ds1]] rho(x1)
x [[ds2]] rho(x1)

About:

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