Extensional case equivalence

[np]

Consider the following:

assert (x : Bool)-> (case x of { `true -> < ?Int > , `false -> < !Int > })
     = (x : Bool)-> < case x of { `true -> ?Int , `false -> !Int } >
     : Type

This is rejected so far but I wish we accept by checking that setting x to true andfalse leads to the resulting terms to be equivalent.

[Danten]

So while I agree that this would be nice, but should we only do this because Bool is not recursive? What criteria can we have, another could be that < _ > commutes with case, but I'm not entirely sure we can just add that and still have the equality be transitive and congurent (I'm not sure what would break or if we even have that now).

A similar situation is, f (case x { true -> e , false -> e' }), which could be equal to case x { true -> f e , false -> f e' }.

[np]

The data-types in Ling are all non-recursive, non-parameterized, non-indexed... They are just a finite enumeration of tags.

My example was with <_> but my intent was wider:

Γ, x : A = `c_i ⊢ t_i = t
-------------------------------------------
Γ, x : A ⊢ case x { `c_i -> t_i } = t

Where the multiple premises form a conjunction.