simp only [trim, untrim_vars]
s : Statement
⊢ trim (untrim s) = trim s
s : Statement
⊢ { ctx := { hyps := (untrim s).ctx.hyps, dj := DJ.trim (untrim s).ctx.dj fun v => v ∈ vars s },
      fmla := (untrim s).fmla } =
    { ctx := { hyps := s.ctx.hyps, dj := DJ.trim s.ctx.dj fun v => v ∈ vars s }, fmla := s.fmla }