GitLab

This issue to keep track of a suggestion by @bbecker to extend destruct to "if .. then .. else":

axiom H: if c1 then c2 else c3 

destruct H would create two branches: one replacing H by c1 and c2 and the other one replacing it with ~c1 and c3.

Note: Similar behavior can be done for match.