case and.mp f g => 
    have l₁ : f ∈ t := canonicalSatisfaction.mp h₁.left
    have l₂ : g ∈ t := canonicalSatisfaction.mp h₁.right
    exact t.property.mpr ⟨BProof.adj (BProof.ax l₁) (BProof.ax l₂)⟩
t : Th
f g : Form
h₁ : t⊨f&g
⊢ f&g ∈ ↑t
no goals