At:
equal appends22
1.
T: Type
2.
a: T List
3.
u: T
4.
v: T List
5.
c,b,d:T List.
(v @ b) = (c @ d) (e:T List. v = (c @ e) & d = (e @ b) c = (v @ e) & b = (e @ d))
6.
c: T List
7.
u1: T
8.
v1: T List
9.
b,d:T List.
[u / (v @ b)] = (v1 @ d)
(e:T List. [u / v] = (v1 @ e) & d = (e @ b) v1 = [u / (v @ e)] & b = (e @ d)) b,d:T List. [u / (v @ b)] = [u1 / (v1 @ d)] (e:T List. [u / v] = [u1 / (v1 @ e)] & d = (e @ b) [u1 / v1] = [u / (v @ e)] & b = (e @ d))
By:
Auto
THEN
SplitCons -1
THEN
InstHyp [v1;b;d] 5
THEN
ParallelOp -1
THEN
ParallelOp -1
THEN
ObviousFrom [-1;-4]
Generated subgoals: