A complete set of tactics
Let us consider formulas build from some set of
variables of sort Prop and the connective ->.
Prove that, if some proposition has a proof in Minimal Propositional
Logic, then some combination using only the tactics
assumption, intro and apply can
prove this proposition.
Look at this file (postscript)