namespace Test

structure Chain (X : Type) where
  pred : ℕ → X → Prop
  nested (k : ℕ) (x : X) (h : pred k x) : pred (k.succ) x

def admissible (X : Type) (c : Chain X) (k : ℕ) (x : X) : Prop :=
  c.pred k x

end Test