fact: Fixpoint list_eq (x y: list A): Prop := match x, y with | nil, nil => True | a :: x', b :: y' => R a b ∧ list_eq x' y' | _, _ => False end.
imports: Coq.Lists.List Coq.Unicode.Utf8 Coq.Setoids.Setoid Coq.Sorting.Permutation Coq.Setoids.Setoid Coq.Classes.Morphisms CoRN.stdlib_omissions.Pair