simp only [trim]
a : List Formula
b : DJ
c : Formula
h : trimmed { ctx := { hyps := a, dj := b }, fmla := c }
⊢ trim { ctx := { hyps := a, dj := b }, fmla := c } = { ctx := { hyps := a, dj := b }, fmla := c }
a : List Formula
b : DJ
c : Formula
h : trimmed { ctx := { hyps := a, dj := b }, fmla := c }
⊢ { ctx := { hyps := a, dj := DJ.trim b fun v => v ∈ vars { ctx := { hyps := a, dj := b }, fmla := c } }, fmla := c } =
    { ctx := { hyps := a, dj := b }, fmla := c }