`redex-check #:satsifying` not self-consistent; related to binding?

I don't even know what to make of this.

#lang racket

(require redex/reduction-semantics)

(define-language Boxy
  (e ::= x (λ (x : t) e) (e e))
  (t ::= nat (→ t t))
  (x u ::= variable-not-otherwise-mentioned)

  (Γ ::= · (x : t Γ))

  #:binding-forms
  (λ (x : t) e #:refers-to x))

(define-judgment-form
  Boxy
  #:mode (type I I O)
  #:contract (type  Γ e t)

  [---------------------
   (type  (x : t Γ) x t)]

  [(type  Γ x_1 t_1)
   ------------------------------------
   (type  ((name x_2 x_!_1) : t_2 Γ) (name x_1 x_!_1) t_1)]

  [(type  (x : t_1 Γ) e t_2)
   -----------------------------------
   (type  Γ (λ (x : t_1) e) (→ t_1 t_2))]

  [(type  Γ e_1 (→ t_1 t_2))
   (type  Γ e_2 t_1)
   -------------------------
   (type  Γ (e_1 e_2) t_2)])

(module+ test
  (require rackunit)
  #|
  counterexample found after 20 attempts:
  (type
   (y : (→ (→ (→ (→ nat nat) nat) (→ (→ nat nat) nat)) nat) (y : (→ nat nat) ·))
   (((λ (e : (→ nat nat)) e) y)
    ((λ (C : nat) C) (y (λ (H : (→ (→ nat nat) nat)) H))))
   nat)
  |#
  (redex-check
   Boxy
   #:satisfying (type  Γ e nat)
   (judgment-holds (type  Γ e nat))))