destruct improvement with if then else
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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information