Nuprl - Proof: l before append iff

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

T:Type, A,B:T List, x,y:T. x before y A @ B x before y A x before y B (x A) & (y B)

By: Unfold `l_before` 0 THEN RWO Thm* C,A,B:T List. C A @ B (A',B':T List. C = (A' @ B') & A' A & B' B) 0

Generated subgoals:

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

2 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 4 steps

About:

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

1	1. `T:` `Type` 2. `A:` `T List` 3. `B:` `T List` 4. `x:` `T` 5. `y:` `T` 6. `A',B':T List. [x; y] = (A' @ B') & A' A & B' B` `[x; y] A [x; y] B (x A) & (y B)`	6 steps

2	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`	4 steps