cases (a_1, ... a_n) \with { ... } should translate to \case a_1 \as x_1 : A_1, ... a_n \as x_n : A_n \return T \with { ... }, where T is the goal in which all occurrences of a_i are replaced with x_i. Similarly, A_j is the type of a_j with replaced occurrences of a_i.
It should be possible to specify positions of a_i, which should be replaced. I'm not sure about the syntax, but it may be something like cases a {3,7} \with { ... } for cases with one argument and cases (a \as x, b \as y, c \as z : (x at 3, y at 2)) {x at (3,7), z at 5} \with { ... } for more than one argument.
cases (a_1, ... a_n) \with { ... }should translate to\case a_1 \as x_1 : A_1, ... a_n \as x_n : A_n \return T \with { ... }, whereTis the goal in which all occurrences ofa_iare replaced withx_i. Similarly,A_jis the type ofa_jwith replaced occurrences ofa_i.It should be possible to specify positions of
a_i, which should be replaced. I'm not sure about the syntax, but it may be something likecases a {3,7} \with { ... }forcaseswith one argument andcases (a \as x, b \as y, c \as z : (x at 3, y at 2)) {x at (3,7), z at 5} \with { ... }for more than one argument.