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

At: paren balance1
T:Type, s':(T+T) List. paren(T;s') (i:T. (inl(i) s') (inr(i) s'))
By: Analyze 0
Generated subgoal:

11. T: Type
s':(T+T) List. paren(T;s') (i:T. (inl(i) s') (inr(i) s'))		6 steps

About:
listunioninlinruniverseimpliesall

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