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

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

None

About:
listconsniluniverseequalandexists

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