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
.