fact: Definition rev_list_rect (A : Type) (P : list A → Type) (H : P []) (H0 : ∀ (a : A) (l : list A), P (rev l) → P (rev (a :: l))) (l : list A) : P (rev l) := list_rect (λ l0 : list A, P (rev l0)) H (λ (a : A) (l0 : list A) (IHl : P (rev l0)), H0 a l0 IHl) l.
imports: Coq.Lists.List Category.Lib.Tactics