PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: mem append

T:Type, L1,L2:T*, t:T. mem_f(T;t;L1 @ L2) mem_f(T;t;L1) mem_f(T;t;L2)
By:
RepD
THEN
ListInd 2
THEN
Reduce 0
THEN
GenExRepD
THEN
Try ProveProp
Generated subgoals:

11. T: Type
2. L1: T*
3. L2: T*
4. t: T
5. u: T
6. v: T*
7. mem_f(T;t;v @ L2) mem_f(T;t;v) mem_f(T;t;L2)
8. mem_f(T;t;v @ L2) (mem_f(T;t;v) mem_f(T;t;L2))
9. mem_f(T;t;v @ L2)
u = t mem_f(T;t;v) mem_f(T;t;L2)
21. T: Type
2. L1: T*
3. L2: T*
4. t: T
5. u: T
6. v: T*
7. mem_f(T;t;v @ L2) mem_f(T;t;v) mem_f(T;t;L2)
8. mem_f(T;t;v @ L2) (mem_f(T;t;v) mem_f(T;t;L2))
9. mem_f(T;t;v)
u = t mem_f(T;t;v @ L2)
31. T: Type
2. L1: T*
3. L2: T*
4. t: T
5. u: T
6. v: T*
7. mem_f(T;t;v @ L2) mem_f(T;t;v) mem_f(T;t;L2)
8. mem_f(T;t;v @ L2) (mem_f(T;t;v) mem_f(T;t;L2))
9. mem_f(T;t;L2)
u = t mem_f(T;t;v @ L2)

About:
alluniverselistorequal