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
A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.