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

At: paren interval 2 1 2 1 1 1 1 1
1. T: Type
2. s1@0: (T+T) List
3. x: T
4. e1: (T+T) List
(inl(x) s1@0 @ [inl(x)] @ e1)
By: Obvious
Generated subgoals:

None

About:
listconsnilunioninluniverse

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