let const
    : ∀(A : Type) → A → ∀(B : Type) → B → A
    = λ(A : Type) → λ(a : A) → λ(B : Type) → λ(_ : B) → a

let example1 = assert : const Natural 5 Natural 10 ≡ 5

in  const