(motive : Lean.Compiler.LCNF.Code Lean.Compiler.LCNF.Purity.pure → Sort u_1) →
  (x : Lean.Compiler.LCNF.Code Lean.Compiler.LCNF.Purity.pure) →
    ((fvarId : Lean.FVarId) →
        (binderName : Lean.Name) →
          (type : Lean.Expr) →
            (funFvarId : Lean.FVarId) →
              (args : Array (Lean.Compiler.LCNF.Arg Lean.Compiler.LCNF.Purity.pure)) →
                (k : Lean.Compiler.LCNF.Code Lean.Compiler.LCNF.Purity.pure) →
                  motive
                    (Lean.Compiler.LCNF.Code.let
                      { fvarId := fvarId, binderName := binderName, type := type,
                        value := Lean.Compiler.LCNF.LetValue.fvar funFvarId args }
                      k)) →
      ((x : Lean.Compiler.LCNF.Code Lean.Compiler.LCNF.Purity.pure) → motive x) → motive x