no goals
ys xs : List Nat
h : xs ≠ []
⊢ sort.loop xs ys ≠ []
induction ys generalizing xs with
| nil => simp [sort.loop]; assumption
| cons y _  ih => simp [sort.loop]; apply ih; apply insert_nonEmpty
case nil
xs : List Nat
h : xs ≠ []
⊢ ¬xs = []
case nil
xs : List Nat
h : xs ≠ []
⊢ sort.loop xs [] ≠ []
simp [sort.loop]
no goals
case nil
xs : List Nat
h : xs ≠ []
⊢ ¬xs = []
assumption
case cons
y : Nat
tail✝ : List Nat
ih : ∀ (xs : List Nat), xs ≠ [] → sort.loop xs tail✝ ≠ []
xs : List Nat
h : xs ≠ []
⊢ ¬sort.loop (insert y xs) tail✝ = []
case cons
y : Nat
tail✝ : List Nat
ih : ∀ (xs : List Nat), xs ≠ [] → sort.loop xs tail✝ ≠ []
xs : List Nat
h : xs ≠ []
⊢ sort.loop xs (y :: tail✝) ≠ []
simp [sort.loop]
case cons.h
y : Nat
tail✝ : List Nat
ih : ∀ (xs : List Nat), xs ≠ [] → sort.loop xs tail✝ ≠ []
xs : List Nat
h : xs ≠ []
⊢ insert y xs ≠ []
case cons
y : Nat
tail✝ : List Nat
ih : ∀ (xs : List Nat), xs ≠ [] → sort.loop xs tail✝ ≠ []
xs : List Nat
h : xs ≠ []
⊢ ¬sort.loop (insert y xs) tail✝ = []
apply ih
no goals
case cons.h
y : Nat
tail✝ : List Nat
ih : ∀ (xs : List Nat), xs ≠ [] → sort.loop xs tail✝ ≠ []
xs : List Nat
h : xs ≠ []
⊢ insert y xs ≠ []
apply insert_nonEmpty