CoRN.logic.PropDecid
Decidability of connectives
Here we show the decidability of logical connectives.
Lemma
imp_dec
: (
∀
A
B
, (
{
A
}
+
{
¬
A
}
) → (
{
B
}
+
{
¬
B
}
) → (
{
A
→
B
}
+
{
~(
A
→
B
)
}
)).
Proof
.
tauto
.
Qed
.