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

At: paren interval 1
1. T: Type
no_repeats(T+T;nil) (s1,s2,s3:(T+T) List, x:T. nil = (s1 @ [inl(x)] @ s2 @ [inr(x)] @ s3) paren(T;s2))
By: Obvious
Generated subgoals:

None

About:
listconsnilunioninlinruniverseequalimpliesall

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