Nuprl - Proof: assert-member-right-paren 1

(3steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: assert-member-right-paren 1

1. T: Type
2. E: TT
3. x,y:T. E(x,y) x = y
4. i: T
5. s: (T+T) List
6. i1: ||s||
7. InjCase(s[i1]; a. false, E(a,i))

i@0:. i@0 < ||s|| & inr(i) = s[i@0]

By: MoveToConcl -1 THEN GenConcl (s[i1] = x) THEN Analyze -2 THEN Reduce 0

Generated subgoal:

1 7. y: T
8. s[i1] = inr(y)
9. E(y,i)
i@0:. i@0 < ||s|| & inr(i) = s[i@0] 1 step

About:

(3steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc