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