Nuprl - Pf record_select_wf_decls

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

ds:Collection(dec()), rho:Decl, s:{[[ds]] rho}, x:Label, t:SimpleType. t dec_lookup(ds;x) s.x [[t]] rho

By: Unfolds [`record`;`r_select`] 0 THEN Unfold `decl_type` 0 THEN Try (Fold `decl` 0) THEN Try (BackThru Thm* ds:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x) , a:SimpleType. mk_dec(x, a) ds y [[a]] rho)

Generated subgoal:

1 1. ds: Collection(dec())
2. rho: Decl
3. s: l:Label[[ds]] rho(l)
4. x: Label
5. t: SimpleType
6. t dec_lookup(ds;x)
mk_dec(x, t) ds

About:

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