title: {assumption, apply, intro} is sufficient for min prop logic
body: <p>I read that the set <code>{assumption, apply, intro}</code> of tactics from <code>Ltac</code> is sufficient to prove any tautology in the minimal constructive propositional logic.</p>
  
  <p>I suppose that a <em>pen-and-paper</em> proof of this claim is done by induction on the syntax of a tautology by showing that the 3 tactics can build incrementally a term that represent the tautology.</p>
  
  <p>I am interested to know if an alternative proof <strong>inside</strong> Coq using <code>Ltac</code> or other meta-language could be possible.</p>
  
  <p>It would mean that Ltac or an alternative meta-language could reflect on what these tactics really do and could manipulate them as variables.</p>
  
  <p>I am much interested in a positive answer in this direction even if it is a bit contrived.</p>