case impl.mpr f g => 
  intros r h₂
  have l₁ := canonicalSatisfaction.mp h₂
  have l₂ : g ∈ (formalApplicationFunction t r).val := ⟨f, l₁, h₁⟩
  exact canonicalSatisfaction.mpr l₂
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
⊢ t⊨f⊃g
no goals