How are prime implicates of HORN-Formulas defined?
This equivalence is a somewhat folklore idea in papers about prime implicants. A small proof is presented in the &quot;Definitions&quot; section of this paper.
The idea behind the equivalence is that, if $C$ is not a prime implicant for $\varphi$, then there is a proper subset $C'$ of $C$ (identifying clauses with the set of literals they force) such that $C'$ is an implicant of $\varphi$. But if this is the case, then you can fill $C'$ with the literals in $C \setminus C'$ until it has size $|C| - 1$, and thus, you obtain an implicant that is $C$ minus exactly one literal you &quot;dropped&quot;. The other direction of the equivalence is trivial: if no proper subset of $C$ is an implicant, then dropping any literal of $C$ gives you something that is not an implicant.
I don't see the relation with Horn formulas, as the equivalence is about definitions for prime implicants of any formula.