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

At: paren balance1 1 3 1
1. T: Type
2. s': (T+T) List
3. t: T
4. i:T. (inl(i) s') (inr(i) s')
5. paren(T;s')
6. i: T
7. inl(i) = inl(t) T+T (inl(i) s') inl(i) = inr(t) T+T
inr(i) = inl(t) T+T (inr(i) s') inr(i) = inr(t) T+T
By: Obvious
Generated subgoals:

None

About:
listunioninlinruniverseequalimpliesorall

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