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

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

None

About:
listdecidableunioninlinruniverseequalall

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