我正在尝试证明逻辑语句r → (∃ x : α,r)，其中r是Prop（命题或陈述），而α是Type 。通过本书的练习，我已经在“精益”中证明了一些东西，但是我坚持这一点。

我真的不确定我什至理解为什么这是真的。由于没有α类型的x，α不会无人居住吗？

我最好的“尝试”是1）希望精益细化者能满足我的需求，

theorem t5_2: r → (∃ x : α,r) :=
  assume rx: r,⟨_,rx⟩

但是它不能推断出类型α的东西，这是有道理的。 2）我还认为这可能是非构造性的证明，因此我在考虑通过矛盾进行证明。但是，我在纸上最远的地方是

  ¬ (∃ x : α,r) → (∀ x : α,¬ r) → ??

我不确定如何精益地执行第一个含义，即使我这样做了，我仍然需要类型为x的{​​{1}}才能消除α。 / p>

任何提示将不胜感激。