It does not look provable, unless you assume forall x y : Set, {x = y} + {x ≠ y} as an axiom (but I have never seen anyone doing that and that's what probably @Dominique mean).

  Lemma example3 (n n' : nat) : @existT Set (fun x => x) nat n = 
    @existT Set (fun x => x) nat n' -> n = n'.
  Proof.
    intro e.
    eapply Eqdep_dec.inj_pair2_eq_dec in e.
    exact e.