fact: Fixpoint is_prefix (A : Type) (A_eq_dec : forall x y : A, {x = y} + {x <> y}) (xs ys : list A) : bool := match xs, ys with | [], _ => true | x :: xs, y :: ys => proj1_sig (Sumbool.bool_of_sumbool (A_eq_dec x y)) && is_prefix A_eq_dec xs ys | _, _ => false end.
imports: Coq(Lia Lists.List) Equations(Equations)