Nuprl - Pf assert_st

(9steps) PrintForm Definitions Lemmas mb automata 1 Sections GenAutomata Doc

1. s1: SimpleType
2. u: SimpleTypeType{i'}
3. w: s1:{v:SimpleType| u(v) }s2:SimpleType. st_eq(s1;s2) s1 = s2
4. x: Label+Unit
5. s2: SimpleType
6. u1: SimpleTypeType{i'}
7. w1: s2:{v:SimpleType| u1(v) }st_eq(tree_leaf(x);s2) tree_leaf(x) = s2
8. x1: Label+Unit
9. InjCase(x; x'. InjCase(x1; y'. x' = y'; b. false); a. InjCase(x1; y'. false; b. true))

tree_leaf(x) = tree_leaf(x1) SimpleType

By: Analyze 8 THEN Analyze 4 THEN All Reduce THEN Try Trivial THEN Try (Fold `typ` 0)

Generated subgoals:

1 4. x3: Label
5. s2: SimpleType
6. u1: SimpleTypeType{i'}
7. w1: s2:{v:SimpleType| u1(v) }st_eq(tree_leaf(inl(x3));s2) tree_leaf(inl(x3)) = s2
8. x2: Label
9. x3 = x2
x3 = x2

2 4. y1: Unit
5. s2: SimpleType
6. u1: SimpleTypeType{i'}
7. w1: s2:{v:SimpleType| u1(v) }st_eq(tree_leaf(inr(y1));s2) tree_leaf(inr(y1)) = s2
8. y: Unit
9. True
tree_leaf(inr(y1)) = tree_leaf(inr(y)) SimpleType

About:

(9steps) PrintForm Definitions Lemmas mb automata 1 Sections GenAutomata Doc

1	4. `x3:` `Label` 5. `s2:` `SimpleType` 6. `u1:` `SimpleTypeType{i'}` 7. `w1:` `s2:{v:SimpleType\| u1(v) }st_eq(tree_leaf(inl(x3));s2) tree_leaf(inl(x3)) = s2` 8. `x2:` `Label` 9. `x3 = x2` `x3 = x2`
2	4. `y1:` `Unit` 5. `s2:` `SimpleType` 6. `u1:` `SimpleTypeType{i'}` 7. `w1:` `s2:{v:SimpleType\| u1(v) }st_eq(tree_leaf(inr(y1));s2) tree_leaf(inr(y1)) = s2` 8. `y:` `Unit` 9. `True` `tree_leaf(inr(y1)) = tree_leaf(inr(y)) SimpleType`