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

At: decidable l member paren 1
1. T: Type
2. x,y:T. Dec(x = y)
3. s: (T+T) List
4. i: T
y:T+T. Dec(inl(i) = y)
By: UnivCD
Generated subgoal:

15. y: T+T
Dec(inl(i) = y)		3 steps

About:
listdecidableunioninluniverseequalall

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