theorem LogicGL.ProvableHilbert.project {α : Type u} {A : Formula α} (h : ⊢ʰ[GL] A) : ⊢ʰ[GL] A.projectEmpty

theorem LogicGL.ProvableHilbert.lift {α : Type u} {B : LetterlessFormula} (h : ⊢ʰ[GL] B) : ⊢ʰ[GL] B.lift