Q:

Figuring out all functions parameter pattern matches

Having:
data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

data One : Bin → Set where
  one : One (x1 nil)
  y0_ : ∀ {bin : Bin} → One bin → One (x0 bin)
  y1_ : ∀ {bin : Bin} → One bin → One (x1 bin)

one-ident : ∀ {x : Bin} → One x → to (from x) ≡ x

What is the logic that generates all the functions parameter pattern matches?
one-ident one = {!   !}
one-ident {x0 x} (y0 o) = {!   !}
one-ident {x1 x} (y1 o) = {!   !}

For example knowing the first argument is {x0 x} why does the 2nd argument have to be (y0 o)? Why can't 2nd argument be (y1 o)?
The code example was taken from here.

A:

one-ident : ∀ {x : Bin} → One x → to (from x) ≡ x
one-ident one = {!   !}
one-ident {x0 xx} (y0 o) = {!   !}
one-ident {x1 xx} (y1 o) = {!   !}

When you know that x is x0 xx in one-ident you know that the type of the second argument is One (x0 xx). There is only 1 constructor in One that can have that type, namely y0_.

