Illegal applicatiocoq
The term "eq_ind_r" of type
 "forall (A : Type) (x : A) (P : A -> Prop), P x -> forall y : A, y = x -> P y"
cannot be applied to the terms
 "nat" : "Set"
 "S n0" : "nat"
 "fun n : nat =>
  match n - n0 with
  | 0 => None
  | S _ => match n - n0 - 1 with
           | 0 => Some A
           | S n' => slist_nth_aux G n'
           end
  end = Some A" : "nat -> Prop"
 "eq_refl" : "Some A = Some A"
 "slist_length G" : "nat"
 "H" : "slist_length G = S n0"
The 4th term has type "Some A = Some A" which should be coercible to
 "(fun n : nat =>
   match n - n0 with
   | 0 => None
   | S _ => match n - n0 - 1 with
            | 0 => Some A
            | S n' => slist_nth_aux G n'
            end
   end = Some A) (S n0)".

Lemma nth_snoc:
  forall {X: Type} (n : nat) (G : slist X) (A : X),
  slist_length G = n -> (G, A)!n = Some A.
Proof.
intro X.
induction n.
- intros.
  apply length_empty in H.
  rewrite H.
  reflexivity.
- intros.
  unfold slist_nth.
  simpl.
  rewrite H.
  change_no_check (S n - n) with (S 0).
  reflexivity.
Qed.

1 subgoal
X : Type
n : nat
IHn : forall (G : slist X) (A : X), slist_length G = n -> (G, A) ! n = Some A
G : slist X
A : X
H : slist_length G = S n
______________________________________(1/1)
match S n - n with
| 0 => None
| S _ => match S n - n - 1 with
         | 0 => Some A
         | S n' => slist_nth_aux G n'
         end
end = Some A

Lemma nth_concat:
  forall {X: Type} (G' G: slist X) (k: nat),
  k < (slist_length G) -> (G;G')!k = G!k.

Inductive slist (X: Type): Type :=
 | empty : slist X
 | snoc : slist X -> X -> slist X.

Fixpoint slist_nth_aux {X : Type} (l : slist X) (n : nat)
                   : option X :=
  match l with
  | empty => None
  | G', x => match n with
               | 0 => Some x
               | S n' => slist_nth_aux G' n'
               end
  end.

Global Hint Unfold slist_nth_aux : slist.

Definition slist_nth {X : Type} (l : slist X) (n : nat) : option X :=
  match slist_length l - n with
  | 0 => None
  | other => slist_nth_aux l (slist_length l - n - 1)
  end.

Notation " G ! n " := (slist_nth G n) (at level 20).

Fixpoint conc {X: Type} (G G': slist X) : slist X :=
  match G' with
  | empty => G
  | snoc D q => snoc (conc G D) q
  end.

Global Hint Unfold conc : slist.

Notation " G ; D " := (conc G D) (at level 20).