inductive seq (α: Type) : Type
| cons : α -> seq -> seq
| nil {} : seq

open seq

def apply {α β} (f: α -> β) : seq α -> seq β
| nil := nil
| (cons x rst) := cons (f x) (apply rst)

theorem apply_singleton {α β} :
  forall (f: α -> β) (x: α),
    apply f (cons x nil) = cons (f x) nil :=
begin
intros,
refl,
end

def size {α: Type} : seq α -> nat
| nil := 0
| (cons _ rst) := size rst + 1

def head {α} (l: seq α) : (0 < size l) -> α :=
begin
intro H,
induction l with x rst,
case seq.cons { exact x },
case seq.nil  { unfold size at H, exfalso, cases H }
end