case cons _ _ h_ind =>
  rw [h_ind]; intros; exact Iff.rfl
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
h_ind : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
⊢ forAll (fun x => r x head✝) as → (List.forAllRel r (reverse as) tail✝ ↔ List.forAllRel r as tail✝)
no goals