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 one can prove it interactively, using only the tactics assumption, intro and apply.

Solution

Look at this file (postscript)