Exercise logic.propositional.consequence

Description
Prove that formula is a logical consequence of a set of formulas

Derivation

~p -> ~q, q => p

⇒ conj-intro, initial=TList [TCon logic1.implies [TCon logic1.not [TVar "p"],TCon logic1.not [TVar "q"]],TVar "q"]

(~p -> ~q) /\ q => p

⇒ logic.propositional.defimpl

(~~p || ~q) /\ q => p

⇒ logic.propositional.notnot

(p || ~q) /\ q => p

⇒ fakeabsorption

p /\ q => p

⇒ conj-elim

p => p