title: How to use Implies and if boolean commands in z3 python API
body: <p>How to implement <code>if-then-else</code> using Z3 python API as a part of conjunction of first order formulas? e.g.</p>
  
  <pre><code>s.add( F, H, (if then else)).
  </code></pre>
  
  <p>A related question is: how to use Boolean "Implies" or "if" commands given in Z3 python online guide for this purpose?</p>