Decidability of connectives
Here we show the decidability of logical connectives.
Lemma
imp_dec
: (
forall
A
B
, ({
A
} + {~A}) -> ({
B
} + {~B}) -> ({
A
->
B
} + {~(A ->
B
)})).