una "contrazione" è l'omotopia che realizza quella contrazione
It seems a bit circular, but I got it.
Since \(A\) is contractible, \(\mathrm{id}_A : A \to A\) is homotopic to some constant map \(k : A \to A\) that has all the elements of \(A\) sent to a certain \(x_0 \in A\). Now consider a homotopy \(C : A \times I \to X\) from \(i \circ \mathrm{id}_A\) to \(i \circ k\), where \(i\) is the inclusion \(A \to X\). If we involve \(\mathrm{id}_X\), we have \(i \circ \mathrm{id}_A = \mathrm{id}_X \circ i\), so that we can employ the asumption \(X\) has HEP: there exists some homotpy \(H : X \times X \to X\) from \(\mathrm{id}_X\) such that
this commutes. The interesting part is \(H(\cdot, 1)\) which maps the elements of \(A\) toward \(x_0\) and can be factored as \(q \circ p\), with \(p : X \to X/A\) being the canonical projection and \(q : X/A \to X\) the unique one that can there be. At this point we have \(q \circ p\) is homotopic to \(\mathrm{id}_X\); the homotopy \(p \circ q \simeq \mathrm{id}_{X/A}\) is immediate (actually, it is an equality).