Nuprl - Pf decls_mng_singleton 1 1 1 1 1

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

1. l1: Label
2. d3: SimpleType
3. rho: Decl
4. s: l:Labelif l = l1 [[d3]] rho else Top fi
5. x1: Label
6. x: if x1 = l1 [[d3]] rho else Top fi
7. lbl: Label
8. d2: SimpleType
9. < lbl,d2 > = < l1,d3 > dec()

lbl = l1 & d2 = d3

By: Fold `mk_dec` -1

Generated subgoals:

1 9. mk_dec(lbl, d2) = mk_dec(l1, d3)
lbl = l1

2 9. mk_dec(lbl, d2) = mk_dec(l1, d3)
d2 = d3

About:

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

1	9. `mk_dec(lbl, d2) = mk_dec(l1, d3)` `lbl = l1`
2	9. `mk_dec(lbl, d2) = mk_dec(l1, d3)` `d2 = d3`