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

At: paren order1 1
1. T: Type
i:T, s1,s2:(T+T) List. nil = (s1 @ [inl(i)] @ s2) (inr(i) s2)
By: Obvious
Generated subgoals:

None

About:
listconsnilunioninlinruniverseequalimpliesall

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