#2.1 The difficulties in the removal of logical parts

A potential danger induced by removal of logical parts is that this removal can modify the evaluation order.
Let us take for example a function of type $\forall x : A, (P x) \to B$, with $A$ and $B$ being informative types, and $P$ a logical property. 
Our function $f$ thus awaits an informative argument and $x$ and a proof that this argument satisfies the pre-condition $P x$. 
If one also has a term $t$ of type $A$ and a proof $p$ of type $(P t)$, one can then form the two well-typed Coq terms $(f~t)$ and $(f~t~p)$.
On the Coq level, these two terms have appreciably different nature.
For example, the evaluation of $(f t)$ will probably be quickly blocked by the lack of the second argument $p$, whereas $(f~t~p)$ is a total application which can normally be reduced towards a value of type $B$ (when for example these terms $f$, $t$ and $p$ are closed).