Below, step by step, I will try to describe the full course of reasoning that will allow to prove pigeonhole_principle_NO_EM, thus answering your questions. Since the whole reasoning is quite large, I will only give the main points of the reasoning, and will post the full version on Github Gist.

So let's get started. Let's say we have

Inductive repeats {X:Type} : list X -> Prop :=
  | repeats0 x l (H: In x l): repeats (x :: l)
  | repeats1 x l (H: repeats l): repeats (x :: l)

Let us now try to carry out the proof without using the excluded middle.

Theorem pigeonhole_principle_no_Em:
  forall (X:Type) (l1  l2:list X), (forall x, In x l1 -> In x l2) ->
  length l2 < length l1 -> repeats l1.
Proof.
  intros X l1. induction l1 as [|x l1' IHl1'].
  { intros l2 H1 H2. simpl in H2. inversion H2. }
  { intros l2 H1 H2.  destruct l2 as [|y l2'].
    - specialize H1 with x. exfalso. apply H1. left. reflexivity.
    - Abort.

Consider what we have before executing Abort:

• We have an inductive hypothesis

  IHl1' : forall l2 : list X, (forall x : X, In x l1' -> In x l2) -> length l2 < length l1' -> repeats l1'

• As well as two auxiliary hypotheses:

  H1 : forall x0 : X, In x0 (x :: l1') -> In x0 (y :: l2')

  H2 : length (y :: l2') < length (x :: l1')

• We are required to prove repeats (x :: l1').

It is easy to see that if we apply repeats1, we can apply IHl1' specialised l2'. We can prove that length l2' < length l1' from H2. But proving (forall x : X, In x l1' -> In x l2) is harder. Logically, we should prove this expression using H1. To do this, we need to study in more detail what an expression of the form forall x : X, In x l1' -> In x l2 is in general, but before that, let us explain why we decided to use destruct l2.

The inductive hypothesis requires that length l2 < length l1', where l2 we specialise. It turns out that if we specialise l2 directly, then we have to prove length l2 < length l1' while having length l2 < length (x::l1'), which obviously cannot be done, so we have to disassemble l2 into x::l2' and use the inductive hypothesis with l2'.

Let us now consider expressions of the form forall x : X, In x l1 -> In x l2. If we rewrite this expression in a more usual form: (∀x (x ∈ l1 ⇒ x ∈ l2)) ⇔ (l1 ⊆ l2) it will be immediately clear that this is nothing else but the notion of a subset relation. There are many facts about this relation that will help us. Let us first introduce the definition in Coq for convenience, and then prove the auxiliary statements. Let's call the relation by html mnemonics.

Definition sube {X : Type} (l1 l2 : list X) := 
  forall x : X, In x l1 -> In x l2.

See Github Gist for more details.

Now let's consider sube. sube (x::l1) (y::l2) is forall z : X, In z (x :: l1) -> In z (y :: l2)

If x = y, then

• if x is not a member of l1, then we can safely exclude x and y from the left parts of the expression.
• if x is a member of l1 (In x l1'), this is enough, since in terms of pigeonhole_principle_no_Em, we need to prove repeats(x::l1'), by applying repeats0 we need to prove [In x l1'], since we apply sube_split to l1', we get exactly what we need.

If x != y, then In x l2 is necessarily satisfied. Further

• if x is a member of l1 (In x l1), then similarly to the previous second point we have proved what is required.
• if x is not a member of l1, then we can discard x:: in the left-hand side of our expression, that is, we get sube l1 (y::l2).

Thus, we obtain the following theorem:

Theorem sube_split : forall {X : Type} (x y : X) (l1 l2 : list X),
  sube (x::l1) (y::l2) ->
  (x = y /\ (In x l1 \/ sube l1 l2)) \/
  (In x l2 /\ sube l1 (y::l2)).
Proof.

See Github Gist for proof of theorem.

Now we are left with one problematic case -- (In x l2 /\ sube l1 (y::l2)], which decomposes into the following cases (applying sube_split2)

• In x l2 /\ In y l1 (logical OR)
• In x l2 /\ sube l1 l2

There is no problem with the second subparagraph, but what about the first one? Let's apply the hint left to us by the authors of the problem, namely in_split. Then we get:

  In x l2 -> exists xl xr, l2 = xl ++ x :: xr.
  In y l1 -> exists yl yr, l1 = yl ++ y :: yr.

Then sube (x::l1) (y::l2) we can write as

sube (x::(yl++y::yr)) (y::(xl++x::xr))

Consider again the question of membership of x.

• If x is a member of l1 = yl ++ y :: yr (In x l1), then we are satisfied and prove pigeonhole_principle_no_Em.
• If x is not a member of l1 = yl ++ y :: yr, then we can discard x:: in the left-hand side, and it also means that l1 is a subset of y::xl ++ xr, so in our notations this means that sube l1 (y::xl ++ xr) is true.

Here in the second case, although we did not get sub l1 l2, we also reduced the original sube (x:::(yl++y::yr)) (y:::(xl++x::xr)) by one sube (yl++y::yr) (y::xl::xr)). Let us put this statement in a separate lemma.

Lemma  sube_split5 : forall {X : Type} (x y : X) (xl xr yl yr: list X),
  sube (x::yl++y::yr) (y::xl++x::xr) -> 
  (In x (yl++y::yr) \/ sube (yl++y::yr) (y::xl++xr)).
Proof.

See Github Gist for proof of theorem.

Let's apply sube_split and prove pigeonhole_principle_no_Em In order not to give a completely ready-made solution, I only give the skeleton of the proof. However, I am sure that if you have read all the steps of the reasoning carefully, you can easily recover the omissions. (You will probably have different names somewhere when using destruct so feel free to change the phrases left out.)

Theorem pigeonhole_principle_no_Em:
  forall (X:Type) (l1  l2:list X),
  (forall x, In x l1 -> In x l2) ->
  length l2 < length l1 ->
  repeats l1.
Proof.
  intros X l1. induction l1 as [|x l1' IHl1'].
  { intros l2 H1 Hlen. simpl in Hlen. inversion Hlen. }
  { intros l2 H1 Hlen.  destruct l2 as [|y l2'].
    - specialize H1 with x. exfalso. apply H1. left. reflexivity.
    - apply sube_split in H1 as H. destruct H as [[Heq H] | H].
      + (* First case: Heq : x = y  и 
        H : In x l1' \/ sube l1' l2' *) 
        
        * 
        * 
          -- (* forall z : X, In z l1' -> In z l2' *)
             
          -- (* length l2' < length l1' *)
             
             
      + (* Second case: H : In x l2' /\ sube l1' (y :: l2') *) 
        
        * (* Third case: HIn1 : In x l2' HIn2 : In y l1' *) 
          apply in_split in HIn1.
          destruct HIn1 as [xl [xr Hx]].
          apply in_split in HIn2.
          destruct HIn2 as [yl [yr Hy]].

          (* We apply sube_split5, but in order not to lose H1, we'll make 
            this application stand out in H2*)

          assert (In x (l1') \/ sube (l1') (y::xl ++ xr)) as H2.  
          { 
            apply sube_split5 in H1. 

          }
          destruct H2 as [HIn | Hs].
          -- 
          --  
             
             ** 
             ** 
             
        * (* Fourth case: HIn1 : In x l2'  Hs : sube l1' l2' *)
          apply repeats1. apply IHl1' with l2'.
          -- (* forall z : X, In z l1' -> In z l2' *)
             
             
          -- (* length l2' < length l1' *)
             
             
  }
Qed.