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

At: paren wf 1
1. T: Type
2. n:
3. s: (T+T) List
4. s1:(T+T) List. ||s1|| < ||s|| paren(T;s1) Prop
5. t: T
6. s': (T+T) List
7. s = ([inl(t)] @ s' @ [inr(t)])
paren(T;s') Type
By: BackThruSomeHyp
Generated subgoal:

1 ||s'|| < ||s||1 step

About:
listconsnilless_thanunioninlinr
universeequalmemberpropimpliesall

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