Agda2

[voidex]

Ковыряю Agda2
module if where open import proof open import bool open import list if_then_else_ : ∀ {l} {a : Set l} → (p : bool) → ((p ≡ true) → a) → a → a if true then t else f = t refl if false then t else f = f head₀ : ∀ {l} {a : Set l} → (ls : list a) → (not (empty ls) ≡ true) → a head₀ {_} {_} null () head₀ {_} {_} (cons x xs) p = x test₁ : ∀ {l} {a : Set l} → list a → a → a test₁ ls v = if (not (empty ls)) then head₀ ls else v test₂ : ∀ {l} {a : Set l} → a → a test₂ v = head₀ (singleton v) refl