P:(((T+T) List)
Prop). P(nil) 
(s1,s2:(T+T) List. P(s1) P(s2) paren(T;s1) paren(T;s2) P(s1 @ s2)) (s:(T+T) List, t:T. P(s) paren(T;s) P([inl(t)] @ s @ [inr(t)])) (s:(T+T) List. paren(T;s) P(s))is mentioned by
| Thm* P:(((T+T) List)Prop). P(nil) (s1,s2:(T+T) List. P(s1) P(s2) paren(T;s1) paren(T;s2) P(s1 @ s2)) (s:(T+T) List, t:T. P(s) paren(T;s) P([inl(t)] @ s @ [inr(t)])) (s:(T+T) List. paren(T;s) P(s)) | [paren_induction] |
In prior sections: core well fnd int 1 bool 1 int 2 rel 1 num thy 1 list 1 mb nat mb list 1 mb list 2 graph 1 1 sqequal 1
Try larger context:
Graphs