# 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