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.

Solution

Look at this file (postscript)

Going home

Pierre Castéran