fact: Definition enumerate_fun_beq (enumerate : list A) (f g : A -> B) : bool := Nat.eqb (List.length (List.filter (fun x => negb (beq (f x) (g x))) enumerate)) 0.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.StringFacts Fiat.Common.Equality Fiat.Common