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

At: decidable l member paren 1 1 1
1. T: Type
2. x,y:T. Dec(x = y)
3. s: (T+T) List
4. i: T
5. x: T
Dec(inl(i) = inl(x) T+T)
By:
InstHyp [i;x] 2
THEN
Obvious
Generated subgoals:

None

About:
listdecidableunioninluniverseequalall

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