class Sokoban.AlwaysMovable (s : State) extends Sokoban.sys.WF s : Prop

• h : ∃ (s_1 : Sokoban.State), Sokoban.sys.Initial s_1 ∧ Sokoban.sys.Reachable s_1 s
• h₁ (s₁ : State) : sys.Reachable s s₁ → ∃ (s₂ : State), sys.Reachable s₁ s₂ ∧ s₁.boxes ≠ s₂.boxes

class Sokoban.MovableBoxConjecture : Prop

• h : ∃ (s : State), AlwaysMovable s