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.