case cons h t => 
constructor
generalize t.reverse = rt
. intro q
  let u := nonEmptyAppend q
  contradiction
. generalize up: List.reverse t ++ [h] = u
  intro q
  cases u <;> simp at q <;> simp
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ List.reverse t ++ [h] = [] ↔
    (match List.reverse t ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none
no goals