How to prove that two empty lists have the same elements in the same order using vacuous implication? I know that to some extent this question may be insignificant, but I'm a little bit uncomfortable with the vacuous implication in this situation.
We know that two lists are equal iff they have the same length and the same elements in the same order. And we know that two empty lists are equal.
So how could we formally prove that two empty lists have the same elements in the same order?
(I think somehow vacuous implication could prove it, but I'm a little bit confused about how to construct the implication since we need to account for the order and the multiplicity of the elements in a list)
 A: If two lists both have length $17$, how can we establish that they "have the same elements in the same order"? What does that phrase mean?
One possible way to say two lists $A$ and $B$ have the same elements is, for all $x$,
$x$ is in $A$ if and only if $x$ is in $B.$
A possible way to say that the elements of $A$ and $B$ are in the same order,
given that they have the same elements, is that for all $x$ and $y$, $x$ and $y$ are in $A$ and $x$ occurs before $y$ in $A$ if and only if $x$ and $y$ are in $B$ and $x$ occurs before $y$ in $B$.
If $A$ and $B$ are empty then for all $x$ and $y$, $x$ does not occur in $A$ and $x$ does not occur in $B$, hence both directions of the implication for "same elements" are vacuously true.
Also, it is not true that $x$ and $y$ are in $A$ and also not true that $x$ and $y$ are in $B$, hence both directions of the implication for "same order" are vacuously true.

The ideas above seem to work if a list is an ordered set (with no repetition of elements) but not if repetition of elements is allowed.
So you probably need something different.
But it really depends on how you define a list in the first place.
A list of length $N$ might be defined a function from the first $N$ integers to the elements of the list.
For example, suppose we say $A$ is a list if there exists a unique non-negative integer $N$ called the length of $A$,
such that if $k$ is an integer, $1 \leq k \leq N,$
then the $k$th element of $A$ exists and may be called $A(k).$
Then $A$ and $B$ have the same elements in the same order if their lengths are the same number $N$ and if $A(k) = B(k)$
for every integer $k$ where $1\leq k\leq N.$
Can you see how this is satisfied vacuously if $N= 0$?
But a list $A$ might be defined inductively as follows:
either $A$ is the empty list (containing no elements),
or $A$ is the ordered pair $(a,A')$ where $a$ is the first element of $A$ and $A'$ is a list.
That is, we make lists by inserting elements at the beginnings of existing lists, starting with the empty list.
Now the question is what it means for two such lists to have the same elements in the same order.
We might define this inductively too, that is, $A$ and $B$ are equal if they are both empty or have equal first elements inserted in front of equal lists. But in that case there's no "proof" that empty lists are equal; we had to accept it by definition in order to support the definition of equality for non-empty lists.
The same problem occurs if we define lists recursively by appending elements to existing lists, that is, a list $A$ is either the empty list or $(A',a)$ where $A'$ is a list and $a$ is an element.

So the question that first has to be answered is, what's a list?
Until that is answered with a mathematical definition, no proof is possible.
A: Formally we need to take element from first list and show, that it is in second list in same order. But "take element from first list" is false sentence, so you can finish implication with any sentence, especially with "element is in second list in same order" and implication is true.
Same for reverse:
That all elements from first list are in second in same order is not enough to show lists equality. We need reverse, that all elements from second list are in first in same order. And analogical consideration gives this for second list in same way as for first one.
