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