At: decls mng singleton 1 1 1 1 1 2
1. l1: Label
2. d3: SimpleType
3. rho: Decl
4. s: l:Label
if 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. mk_dec(lbl, d2) = mk_dec(l1, d3)
d2 = d3
By:
ApFunToHypEquands `z' z.typ SimpleType -1
THEN
All Reduce
Generated subgoals:None
About:
