fact: Fixpoint list_eqb@{} (ls rs : list T) : bool := match ls , rs with | nil , nil => true | cons l ls , cons r rs => if l ?[ eq ] r then list_eqb ls rs else false | _ , _ => false end.
imports: Coq.Lists.List ExtLib.Core.RelDec ExtLib.Structures.Monoid ExtLib.Structures.Reducible ExtLib.Tactics.Consider ExtLib.Tactics.Injection ExtLib.Structures.Traversable ExtLib.Structures.Functor ExtLib.Structures.Monads ExtLib.Structures.Applicative