λ(nix : ../NixPrelude.dhall) →
  let Any = ../Any/Type.dhall

  let Any/toAny = ../Any/toAny.dhall nix

  let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix

  let Any/equal = ../Any/equal.dhall nix

  in  λ(t : Type) →
        let FunctionType = λ(x : Type) → x → (t → t) → t → t

        let function =
              λ(function : FunctionType Any) →
                let functionArgs =
                      Any/toTypeUnchecked
                        (FunctionType (FunctionType Any))
                        (Any/toAny (FunctionType Any) function)
                        function

                in  λ(f : t → t) →
                    λ(x : t) →
                      let xp = f x

                      in  if    Any/equal (Any/toAny t xp) (Any/toAny t x)
                          then  x
                          else  functionArgs f xp

        let functionErased =
              Any/toTypeUnchecked
                (FunctionType Any)
                (Any/toAny (FunctionType (FunctionType Any)) function)

        in  function functionErased