Theorem: Notes.sorted_tail_of_sorted (Notes4/IndPred.lean)

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
as : List α
h : Sorted f (a :: as)
⊢ Sorted f as
Tactic:
match h with 
| single => apply nil  
| longer _ h'' => exact h''
State after:
no goals

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
as : List α
h : Sorted f (a :: as)
⊢ Sorted f []
Tactic:
apply nil
State after:
no goals

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
as : List α
h : Sorted f (a :: as)
a₂✝ : α
as✝ : List α
h✝ : f a a₂✝ = true
h'' : Sorted f (a₂✝ :: as✝)
⊢ Sorted f (a₂✝ :: as✝)
Tactic:
exact h''
State after:
no goals