我正在寻找一个看起来像连续两个正斜杠的符号。当然，我可以像这样输入两个斜线： // 但我更喜欢这些斜线非常靠近的单个符号。我试图谷歌它，无济于事。
经过多次失败后，我发现 Coq 做了一件我不明白的奇怪事情。抱歉涉及的代码，我无法隔离一个更简单的示例。我有一个包含trident三个变量的公式p，q, r。a <-> b然后，我简单地用in place of p、ain place ofq和bin place of写出该公式的一个实例r，并尝试证明一个引理，表明结果相当于trident上面的代入。当试图证明我被第一个子目标困住时，它写着
a, b : Prop
H : b
============================
a \/ (a <-> b)
这显然是无法证明的：如果b假设为真，那么就a \/ (a <-> b)变为正义a，并且没有理由它为真。
这是完整的代码：
From Coq Require Import Setoid.
Definition denseover (p q : Prop) := (p -> q) -> q.
Definition trident (p q r …