Nuprl - Pf assert eq relname

(6steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

a,b:relname(). eq_relname(a;b) a = b

By: UnivCD THEN Unfolds [`relname`;`eq_relname`] 0 THEN Analyze 2 THEN Analyze 1 THEN Reduce 0 THEN Try (RWW "assert_st_eq" 0) THEN EqLblFwd THEN Try (Analyze THEN (Complete Auto))

Generated subgoals:

1 1. x1: SimpleType
2. x: SimpleType
3. inl(x1) = inl(x) SimpleType+Label
x1 = x

2 1. y: Label
2. x: SimpleType
3. inr(y) = inl(x) SimpleType+Label
False

3 1. x: SimpleType
2. y: Label
3. inl(x) = inr(y) SimpleType+Label
False

4 1. y1: Label
2. y: Label
3. inr(y1) = inr(y) SimpleType+Label
y1 = y

About:

(6steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

1	1. `x1:` `SimpleType` 2. `x:` `SimpleType` 3. `inl(x1) = inl(x) SimpleType+Label` `x1 = x`
2	1. `y:` `Label` 2. `x:` `SimpleType` 3. `inr(y) = inl(x) SimpleType+Label` `False`
3	1. `x:` `SimpleType` 2. `y:` `Label` 3. `inl(x) = inr(y) SimpleType+Label` `False`
4	1. `y1:` `Label` 2. `y:` `Label` 3. `inr(y1) = inr(y) SimpleType+Label` `y1 = y`