Nuprl - Proof: assert-member-right-paren

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

At: assert-member-right-paren

T:Type, E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-right-paren(x,y.E(x,y);i;s) (inr(i) s))

By: UnivCD THEN Unfold `member-right-paren` 0 THEN RWO Thm* L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i])) 0 THEN Unfold `l_member` 0 THEN ExRepD THEN Try ((((InstConcl [i@0]) THEN (RevHypSubst -1 0)) THEN (Reduce 0)) THEN EasyHyp)

Generated subgoal:

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] 2 steps

About:

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