Universal typing axiom ($\varnothing \mapsto p:\star \text{for every }p$)

An extension of simple type assignment that assigns a distinguished atomic type variable $\star$ to every lambda term in the empty typing context. The recorded assumptions therefore need not contain all free variables of the subject. This is a rule admitting a typing judgment, rather than an implicit conversion to every simple type or a general subtyping rule.