Proof is MLL cut Free

theorem Proof.isMLL_cutFree {Γ : Sequent Atom} (p : ⇓Γ) (hΓ : Γ.IsMLL)    (hp : p.cutFree) : p.IsMLL := by  induction p  case ax => simp_all  case one => simp  case bot _ _ ih =>    refine ih ?_ hp    simpa using hΓ  case parr a b Γ p ih =>    refine ih ?_ hp    simp at hΓ    grind [Sequent.IsMLL]  case tensor a b Γ Δ p q ihp ihq =>    simp at hΓ    refine ⟨ihp ?mll.p ?cut.p, ihq ?mll.q ?cut.q⟩    case mll | mll => grind [Sequent.IsMLL]    case cut | cut => grind [cutFree]  case oplus₁ | oplus₂ | «with» | top | quest | contract | weaken | bang => simp at hΓ  case cut => simp [cutFree] at hp