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

At: paren induction 1
1. T: Type
2. P: ((T+T) List)Prop
3. P(nil)
4. s1,s2:(T+T) List. P(s1) P(s2) paren(T;s1) paren(T;s2) P(s1 @ s2)
5. s:(T+T) List, t:T. P(s) paren(T;s) P([inl(t)] @ s @ [inr(t)])
6. n:
7. s: (T+T) List
8. s1:(T+T) List. ||s1|| < ||s|| paren(T;s1) P(s1)
9. s = nil
P(s)
By: Obvious
Generated subgoals:

None

About:
listconsnilless_thanunioninlinr
functionuniverseequalpropimpliesall

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