case refine_1
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ C nil

case refine_2
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ ∀ (head : α) (tail : List α), C ↑tail → C ↑(head :: tail)
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ C (Quotient.mk'' l)
refine List.recOn l ?_ ?_ <;> simp
no goals
case refine_1
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ C nil

case refine_2
α : Type u_1
C : Cycle α → Prop
s : Cycle α
H0 : C nil
HI : ∀ (a : α) (l : List α), C ↑l → C ↑(a :: l)
l : List α
⊢ ∀ (head : α) (tail : List α), C ↑tail → C ↑(head :: tail)
assumption'