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

At: l before append iff 2 2
1. T: Type
2. A: T List
3. B: T List
4. x: T
5. y: T
6. [x; y] B
A',B':T List. [x; y] = (A' @ B') & A' A & B' B
By:
InstConcl [nil;[x; y]]
THEN
Reduce 0
THEN
Try Obvious
Generated subgoals:

None

About:
listconsniluniverseequalandexists

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