T:Type, C,A,B:T List. C A @ B (A',B':T List. C = (A' @ B') & A' A & B' B)

InductionOnList
THEN
InductionOnList
THEN
Reduce 0
THEN
Try (RWO Thm* L:T List. nil L True 0)
THEN
Try (Auto THEN (InstConcl [nil;nil]) THEN (Reduce 0) THEN (RWO Thm* L:T List. nil L True 0))
THEN
Try ((RWO Thm* L:T List. L nil L = nil 0) THEN ObviousConcl)

1

1. T: Type 2. C: T List 3. u: T 4. v: T List 5. A,B:T List. v A @ B (A',B':T List. v = (A' @ B') & A' A & B' B) 6. A: T List 7. u1: T 8. v1: T List 9. B:T List. [u / v] v1 @ B (A',B':T List. [u / v] = (A' @ B') & A' v1 & B' B) B:T List. [u / v] [u1 / (v1 @ B)] (A',B':T List. [u / v] = (A' @ B') & A' [u1 / v1] & B' B)

15 steps

About: