[NTG-context] lemmas for headers