Lean4
/-- Because the two halves of the definition of `inv` produce more elements
on each side, we have to define the two families inductively.
This is the indexing set for the function, and `invVal` is the function part. -/
inductive InvTy (l r : Type u) : Bool → Type u
| zero : InvTy l r false
| left₁ : r → InvTy l r false → InvTy l r false
| left₂ : l → InvTy l r true → InvTy l r false
| right₁ : l → InvTy l r false → InvTy l r true
| right₂ : r → InvTy l r true → InvTy l r true