IoI is transport

Did we really not ever mention explicitly that these are the same?
Since we prove IoI as a lemma, why don't we skip the "exercise" and rephrase this sentence as: "We will show in \autoref{lem:transport} that indiscernability of identicals is an instance of path induction. There we will also give a new name and notation for indiscernability of identicals."

This way we also tell why it is easy, because it is a special case.