Nuprl - Proof: paren balance1 1 1

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

At: paren balance1 1 1

1. T: Type
2. i: T
3. (inl(i) nil)

(inr(i) nil)

By: Obvious

Generated subgoals:

None

About:

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