Is it possible to force induction tactic to produce more equations?

How to get a solution for the original problem

You can use remember tactic because induction (and destruct) "forgets" the exact shape of indices. And in the type arg1 <<< arg2, both arg1 and arg2 are indices. Incidentally, this blog post by James Wilcox explains how this works in detail. Anyways, if you want to do induction on an inductive type family, you often want the indices to be variables (with extra equations keeping all the information you need).

So, if you start like so:

remember (x :: l1) as xl1 eqn: E1.
remember (y :: l2) as xl2 eqn: E2.

you get your equations, but you will eventually get into trouble because the induction hypotheses won't be usable. To make them usable, simply generalize the induction hypotheses by doing

revert x y l1 l2 E1 E2.

More explicit, you start like so

Lemma subseq_right_elim (X : Type) (l1 l2 : list X) (x y : X) :
  (x :: l1) <<< (y :: l2) -> (x = y) \/ (x :: l1) <<< l2.
X: Type
l1, l2: list X
x, y: X
(x :: l1) <<< (y :: l2) -> x = y \/ (x :: l1) <<< l2
Proof.
X: Type
l1, l2: list X
x, y: X
(x :: l1) <<< (y :: l2) -> x = y \/ (x :: l1) <<< l2
  intros H.
X: Type
l1, l2: list X
x, y: X
H: (x :: l1) <<< (y :: l2)
x = y \/ (x :: l1) <<< l2
  remember (x :: l1) as xl1 eqn: E1.
X: Type
l1, l2: list X
x, y: X
xl1: list X
E1: xl1 = x :: l1
H: xl1 <<< (y :: l2)
x = y \/ xl1 <<< l2 remember (y :: l2) as xl2 eqn: E2.
X: Type
l1, l2: list X
x, y: X
xl1: list X
E1: xl1 = x :: l1
xl2: list X
E2: xl2 = y :: l2
H: xl1 <<< xl2
x = y \/ xl1 <<< l2
  revert x y l1 l2 E1 E2.
X: Type
xl1, xl2: list X
H: xl1 <<< xl2
forall (x y : X) (l1 l2 : list X),
xl1 = x :: l1 -> xl2 = y :: l2 -> x = y \/ xl1 <<< l2
  induction H as [| l1' l2' z S IH | l1' l2' z S IH]; intros x y l1 l2 E1 E2.
X: Type
x, y: X
l1, l2: list X
E1: [] = x :: l1
E2: [] = y :: l2
x = y \/ [] <<< l2
X: Type
l1', l2': list X
z: X
S: (z :: l1') <<< l2'
IH: forall (x y : X) (l1 l2 : list X),
z :: l1' = x :: l1 ->
l2' = y :: l2 -> x = y \/ (z :: l1') <<< l2
x, y: X
l1, l2: list X
E1: l1' = x :: l1
E2: l2' = y :: l2
x = y \/ l1' <<< l2
X: Type
l1', l2': list X
z: X
S: l1' <<< l2'
IH: forall (x y : X) (l1 l2 : list X),
l1' = x :: l1 ->
l2' = y :: l2 -> x = y \/ l1' <<< l2
x, y: X
l1, l2: list X
E1: z :: l1' = x :: l1
E2: z :: l2' = y :: l2
x = y \/ (z :: l1') <<< l2

For what it's worth, the statement of your lemma is not general enough, so induction won't help -- this time you will be able to solve the third subgoal, but not the second one. To overcome this difficulty, make the lemma's statement more like subseq_left_elim.

SPOILER ALERT: this gist has full proof.

A better way is to redefine inductive predicate

Now, the difficulties you are experiencing stem from the roundabout way to define the notion of being a subsequence. You can see it more clearly from a proof of a very simple example:

Goal [1; 3; 5] <<< [0; 1; 2; 3; 4; 5; 6].
[1; 3; 5] <<< [0; 1; 2; 3; 4; 5; 6]
Proof.
[1; 3; 5] <<< [0; 1; 2; 3; 4; 5; 6]
  apply subseq_left_elim with 0.
[0; 1; 3; 5] <<< [0; 1; 2; 3; 4; 5; 6] apply subseq_intro.
[1; 3; 5] <<< [1; 2; 3; 4; 5; 6] apply subseq_intro.
[3; 5] <<< [2; 3; 4; 5; 6]
  apply subseq_left_elim with 2.
[2; 3; 5] <<< [2; 3; 4; 5; 6] apply subseq_intro.
[3; 5] <<< [3; 4; 5; 6] apply subseq_intro.
[5] <<< [4; 5; 6]
  apply subseq_left_elim with 4.
[4; 5] <<< [4; 5; 6] apply subseq_intro.
[5] <<< [5; 6] apply subseq_intro.
[] <<< [6]
  apply subseq_left_elim with 6.
[6] <<< [6] apply subseq_intro.
[] <<< [] apply empty_subseq.
Qed.

Basically, you have to grow the size of your goal to reduce it later.

Had you chosen a simpler encoding, e.g.

Reserved Notation "l <<< k" (at level 10).
Inductive subseq {X : Type} : list X -> list X -> Prop :=
| empty_subseq : [] <<< []
| subseq_drop_right l1 l2 x : l1 <<< l2 ->       l1  <<< (x :: l2)
| subseq_drop_both l1 l2 x  : l1 <<< l2 -> (x :: l1) <<< (x :: l2)
where "l <<< k" := (subseq l k).

your life would have been so much easier! E.g. here is a new proof of the aforementioned simple fact:

Goal [1; 3; 5] <<< [0; 1; 2; 3; 4; 5; 6].
[1; 3; 5] <<< [0; 1; 2; 3; 4; 5; 6]
  apply subseq_drop_right.
[1; 3; 5] <<< [1; 2; 3; 4; 5; 6] apply subseq_drop_both.
[3; 5] <<< [2; 3; 4; 5; 6]
  apply subseq_drop_right.
[3; 5] <<< [3; 4; 5; 6] apply subseq_drop_both.
[5] <<< [4; 5; 6]
  apply subseq_drop_right.
[5] <<< [5; 6] apply subseq_drop_both.
[] <<< [6]
  apply subseq_drop_right.
[] <<< [] apply empty_subseq.
Qed.

This time you just make the goal smaller with every step you take.