Выяснение соответствия шаблонов параметров всех функций

Question

Имея:

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

Какая логика генерирует совпадения всех шаблонов параметров функций?

one-ident one = {!   !}
one-ident {x0 x} (y0 o) = {!   !}
one-ident {x1 x} (y1 o) = {!   !}

Например, зная, что первый аргумент равен {x0 x}, почему второйаргумент должен быть (y0 o)?Почему второй аргумент не может быть (y1 o)?

Пример кода взят из здесь .

Answer 1

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) = {!   !}

Когда вы знаете, что x равно x0 xx в одном идентификаторе, вы знаете, что тип второго аргумента - One (x0 xx).В One есть только 1 конструктор, который может иметь этот тип, а именно y0_.