Coq using lemma itself for proof

I was solving a Coq problem below, and I'm curious how to re-use lemma itself again (as a hypothesis) for the proof.

Inductive lparen : T -> Prop :=
| leps : lparen eps
| lseq : forall (lp: T) (lp': T), lparen lp /\ lparen lp' -> lparen (LPs +++ lp +++ RPs +++ lp').

(* +++ operator concats between parenthesess *)

Lemma lparen_concat : forall l l':T, lparen l -> lparen l' -> lparen (l +++ l').
Proof.
  intros l l' IHl IHl'.
  induction IHl as [|lp lp' [IHHl IHHl']].
  - simpl.
    assumption.
  - rewrite par_assoc.
    apply lseq.
    split.
    + assumption.
    +
Qed.

The remaining goal is following lparen (lp' +++ l'), which can be proved by applying lparen_concat itself again.

l', lp, lp' : T
IHHl : lparen lp
IHHl' : lparen lp'
IHl' : lparen l'
-----------------------
lparen (lp' +++ l')

Solution

Note that in your proof, when you do induction IHl as [|lp lp' [IHHl IHHl']], that IHHl and IHHl' are not induction hypotheses. The reason is that you wrote your inductive predicate in an uncanonical way, so Coq's default method for inferring the induction scheme fails.

Instead, try defining your inductive predicate like so:

Inductive lparen : T -> Prop :=
| leps : lparen eps
| lseq : forall (lp: T) (lp': T), lparen lp -> lparen lp' -> lparen (LPs +++ lp +++ RPs +++ lp').

The difference being that we give two preconditions lparen lp and lparen lp', instead of one which is a conjunction. In Coq, this is much more natural (since -> is a primitive).

Then, the induction scheme actually contains induction hypotheses, which makes the proof go through:

Lemma lparen_concat : forall l l':T, lparen l -> lparen l' -> lparen (l +++ l').
Proof.
  intros l l' Hl Hl'.
  induction Hl as [|lp lp' Hlp IHlp  Hlp' IHlp']].
  - simpl.
    assumption.
  - rewrite par_assoc.
    apply lseq.
    split.
    + assumption.
    + apply IHlp'.
Qed.

Note that Hlp corresponds to your IHHl, which you named IH even though it is not an induction hypothesis. What I named IHlp' is what was missing in your proof (and actually is an inductive hypothesis), but is here now, since Coq can now generate useful induction schemes for your predicate.

Similarly, the things introd in the first line are not induction hypotheses and thus not named IH by convention.

Finally, note that I would not say that induction is "assuming the Lemma you are proving." It "assumes" a special case of the Lemma, where one argument is strictly smaller than it is in the goal you are currently proving. This is then usually called the inductive hypothesis. So a better way of asking your question is "how do I get Coq to generate the correct inductive hypothesis here?".