fact: Fixpoint list_eq_bool A (eq_bool : A -> A -> bool) (l1 l2 : list A) {struct l1} : bool := match l1 with | nil => match l2 with nil => true | _ :: _ => false end | t1 :: l1 => match l2 with nil => false | t2 :: l2 => andb (eq_bool t1 t2) (list_eq_bool eq_bool l1 l2) end end.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)