apply dependently typed constructor in hypothesis

Consider the following inductive definition:

Inductive T (n : nat) : nat -> Prop :=
  | c1 : T n n.

This works:

Theorem a : T 1 1.
Proof.
  apply c1.
Qed.

But this doesn't:

Theorem b : T 1 1 -> True.
Proof.
   intros H.
   apply c1 in H.

Both calls to apply seem equivalent to me, but the latter fails with Error: Statement without assumptions. Why? And how can I make it work?

Solution

This question arose from my poor understanding of the apply tactic. @gallais's comment made me realize why apply c1 in H doesn't really make sense. The tactic essentially works as a function application on H and c1 H doesn't really make sense. For future reference, this is an example in which apply in would make sense. If we had another constructor c2 like this:

Inductive T (n : nat) : nat -> Prop :=
  | c1 : T n n
  | c2 : forall x, T n x -> T n (S x).

Then apply c2 in H would transform something of type T n x into something of type T n (S x), for example:

Theorem b : T 1 1 -> True.
Proof.
  intros H.
  apply c2 in H.

transforms the hypothesis H : T 1 1 into H : T 1 2.