fact: Fixpoint beq_list {A} (eq : Deq A) (l1 l2 : list A) : bool := match l1, l2 with | [], [] => true | [], _ => false | _, [] => false | x :: xs, y :: ys => if eq x y then beq_list eq xs ys else false end.
imports: UsefulTypes bin_rels Omega