Thinking about this, adapted from a tweet that was meant to infuriate

if e then true else false

Because it's equivalent to e ofc, but really it's a case of:

if e then C[true] else C[false] === C[e]

But also:

if e then (if e then e1 else e2) else (if e then e3 else e4) === if e then e1 else e4

Or generally:

if e then C1[e] else C2[e] === if e then C1[true] else C2[false]

And finally:

C[if e then e1 else e2] === if e then C[e1] else C[e2]

✨ eta laws ✨

At least, the first one is definitely an eta law, since it's the eliminator wrapped around constructors
The third one is a bit dangerous, since e gets evaluated first instead of whatever's in your context C
I feel like the second one should arise from some congruence rules but I can't see how