标签: plfa

postulate
  extensionality : ? {A B : Set} {f g : A ? B}
    ? (? (x : A) ? f x ? g x)
      -----------------------
    ? f ? g

我知道上面的定义是一致的，但是如果稍微改动一下呢？

postulate
  extensionality' : ? {A : Set} {B : A ? Set} {f g : (x : A) ? B x}
    ? (? (x : A) ? f x ? g x)
      -----------------------
    ? f ? g

为了解决 PLFA 书中的一个练习，我必须定义它，但我不确定这样做是否正确。我认为这应该是一致的，但我目前没有一个很好的方法来推理这一点，所以我想在这里问一下。