Nuprl - Proof: l before append iff 2

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

1. T: Type
2. A: T List
3. B: T List
4. x: T
5. y: T
6. [x; y] A [x; y] B (x A) & (y B)

A',B':T List. [x; y] = (A' @ B') & A' A & B' B

By: SplitOrHyps

Generated subgoals:

1 6. [x; y] A
A',B':T List. [x; y] = (A' @ B') & A' A & B' B 1 step

2 6. [x; y] B
A',B':T List. [x; y] = (A' @ B') & A' A & B' B 1 step

3 6. (x A) & (y B)
A',B':T List. [x; y] = (A' @ B') & A' A & B' B 1 step

About:

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

1	6. `[x; y] A` `A',B':T List. [x; y] = (A' @ B') & A' A & B' B`	1 step

2	6. `[x; y] B` `A',B':T List. [x; y] = (A' @ B') & A' A & B' B`	1 step

3	6. `(x A) & (y B)` `A',B':T List. [x; y] = (A' @ B') & A' A & B' B`	1 step