# Why REFL rule is primitive in HOL Light?

HOL Light assumed REFL as a primitive. Why does it need to do so? Can't REFL rule be deduced in this way using ASSUME twice and DEDUCT_ANTISYM_RULE once?

$$\frac{\overline{\{p\}\vdash p} \quad \overline{\{p\}\vdash p}}{\vdash p = p}$$

• I’m not sure, but it’s plausible this is just an optimization. You’d have to apply the above derivation for each desired $p$ separately. – Geoffrey Irving Jun 8 '20 at 18:42