fix some instance names
(λ _ _ : A, x) is not id, it is a two-argument form of const.
(λ x _ : A, x) is not constant, it is the identity in the first argument.
(λ _ _ : A, x) is not id, it is a two-argument form of const.
(λ x _ : A, x) is not constant, it is the identity in the first argument.
