have l₂ : g ∈ (formalApplicationFunction t r).val := ⟨f, l₁, h₁⟩
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
r : Th
h₂ : r⊨f
l₁ : f ∈ ↑r
⊢ t∙r⊨g
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
r : Th
h₂ : r⊨f
l₁ : f ∈ ↑r
l₂ : g ∈ ↑(formalApplicationFunction t r)
⊢ t∙r⊨g