Theorem sublistAt_left ≪ | index | src | ≫ 

theorem sublistAt_left (L1 L2 l n: nat):
  $ sublistAt n L1 L2 -> sublistAt n (L1 ++ l) L2 $;
StepHypRefExpression
1 eqtr 
(a1 ++ L2 ++ a2) ++ l = a1 ++ (L2 ++ a2) ++ l -> a1 ++ (L2 ++ a2) ++ l = a1 ++ L2 ++ a2 ++ l -> (a1 ++ L2 ++ a2) ++ l = a1 ++ L2 ++ a2 ++ l
2 appendass 
(a1 ++ L2 ++ a2) ++ l = a1 ++ (L2 ++ a2) ++ l
3 1, 2 ax_mp 
a1 ++ (L2 ++ a2) ++ l = a1 ++ L2 ++ a2 ++ l -> (a1 ++ L2 ++ a2) ++ l = a1 ++ L2 ++ a2 ++ l
4 appendeq2 
(L2 ++ a2) ++ l = L2 ++ a2 ++ l -> a1 ++ (L2 ++ a2) ++ l = a1 ++ L2 ++ a2 ++ l
5 appendass 
(L2 ++ a2) ++ l = L2 ++ a2 ++ l
6 4, 5 ax_mp 
a1 ++ (L2 ++ a2) ++ l = a1 ++ L2 ++ a2 ++ l
7 3, 6 ax_mp 
(a1 ++ L2 ++ a2) ++ l = a1 ++ L2 ++ a2 ++ l
8 id 
L1 = a1 ++ L2 ++ a2 -> L1 = a1 ++ L2 ++ a2
9 8 anwl 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n -> L1 = a1 ++ L2 ++ a2
10 9 anwl 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ x = a2 ++ l -> L1 = a1 ++ L2 ++ a2
11 eqidd 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ x = a2 ++ l -> l = l
12 10, 11 appendeqd 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ x = a2 ++ l -> L1 ++ l = (a1 ++ L2 ++ a2) ++ l
13 eqidd 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ x = a2 ++ l -> a1 = a1
14 eqidd 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ x = a2 ++ l -> L2 = L2
15 id 
x = a2 ++ l -> x = a2 ++ l
16 15 anwr 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ x = a2 ++ l -> x = a2 ++ l
17 14, 16 appendeqd 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ x = a2 ++ l -> L2 ++ x = L2 ++ a2 ++ l
18 13, 17 appendeqd 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ x = a2 ++ l -> a1 ++ L2 ++ x = a1 ++ L2 ++ a2 ++ l
19 12, 18 eqeqd 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ x = a2 ++ l -> (L1 ++ l = a1 ++ L2 ++ x <-> (a1 ++ L2 ++ a2) ++ l = a1 ++ L2 ++ a2 ++ l)
20 7, 19 mpbiri 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ x = a2 ++ l -> L1 ++ l = a1 ++ L2 ++ x
21 anlr 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ x = a2 ++ l -> len a1 = n
22 20, 21 iand 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n /\ x = a2 ++ l -> L1 ++ l = a1 ++ L2 ++ x /\ len a1 = n
23 22 iexde 
L1 = a1 ++ L2 ++ a2 /\ len a1 = n -> E. x (L1 ++ l = a1 ++ L2 ++ x /\ len a1 = n)
24 23 eex 
E. a2 (L1 = a1 ++ L2 ++ a2 /\ len a1 = n) -> E. x (L1 ++ l = a1 ++ L2 ++ x /\ len a1 = n)
25 24 eximi 
E. a1 E. a2 (L1 = a1 ++ L2 ++ a2 /\ len a1 = n) -> E. a1 E. x (L1 ++ l = a1 ++ L2 ++ x /\ len a1 = n)
26 25 conv sublistAt 
sublistAt n L1 L2 -> sublistAt n (L1 ++ l) L2

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)