by induction hypothesis we know

by induction hypothesis we know P (id)

Synopsis:

by induction hypothesis we know term ( id )

Pre-condition:

The user must have started proving a case for a proof by induction/case-analysis.

Action:

It introduces the inductive hypothesis.

New sequents to prove:

None.