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

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

15. x: T
Dec(inl(i) = inl(x) T+T)		1 step
 
25. y1: T
Dec(inl(i) = inr(y1) T+T)		1 step

About:
listdecidableunioninlinruniverseequalall

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