theorem Sokoban.MovableBoxConjecture.boxes_ne_empty_of_alwaysMovable {s : State} (h : AlwaysMovable s) : s.boxes ≠ ∅

theorem Sokoban.MovableBoxConjecture.alwaysMovable_iff_alt₁ {s : State} : AlwaysMovable s ↔ sys.WF s ∧ s.boxes ≠ ∅ ∧ ∀ (s₁ : State), sys.Reachable s s₁ → ∃ (s₂ : State), sys.Reachable s₁ s₂ ∧ s₁.boxes ≠ s₂.boxes

theorem Sokoban.MovableBoxConjecture.alwaysMovable_of_reachable {s s₁ : State} [H : AlwaysMovable s] (h : sys.Reachable s s₁) : AlwaysMovable s₁