{motive : Lean.Compiler.LCNF.Closure.Context → Sort u} →
  ((inScope abstract : Lean.FVarId → Bool) →
      (isUnderBinder : Bool) → motive { inScope := inScope, abstract := abstract, isUnderBinder := isUnderBinder }) →
    (t : Lean.Compiler.LCNF.Closure.Context) → motive t