If you want to know how it is elaborate, you can always normalize zip:

```
Compute unzip.
Arguments unzip {A}%type_scope l%list_scope
= (fix Ffix (x : Type) (x0 : list (x * x)) {struct x0} :
list x * list x :=
match x0 with
| [] => ([], [])
| x1 :: x2 =>
(let (H, H0) := x1 in
fun (_ : list (x * x)) (x3 : list x * list x) =>
let (H1, H2) := x3 in (H :: H1, H0 :: H2)) x2
(Ffix x x2)
end) ?A
: list (?A * ?A) -> list ?A * list ?A
where
?A : [ |- Type]
```

This topic was moved here from #Coq users > Equations `with`

syntax by Karl Palmskog.

please use #Equations devs & users for questions about Equations

Last updated: Oct 13 2024 at 01:02 UTC