Nuprl - Proof: assert-member-paren

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

At: assert-member-paren

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

By: UnivCD THEN Unfold `member-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 SplitOrHyps 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. E(a,i), E(a,i))
(i@0:. i@0 < ||s|| & inl(i) = s[i@0]) (i@0:. i@0 < ||s|| & inr(i) = s[i@0]) 3 steps

About:

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