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
.