proposition: Lemma is_prefix_correct' : forall (A : Type) (A_eq_dec : forall x y, {x = y} + {x <> y}) (xs ys : list A), is_prefix A_eq_dec xs ys = true <-> xs ++ skipn (length xs) ys = ys.
proof: Proof. intros. split; intro; generalize dependent ys; induction xs; intros; destruct ys; intuition; try discriminate. - apply andb_prop in H as []. fold is_prefix in H0. cbn. rewrite IHxs. + f_equal. destruct (A_eq_dec a a0). * intuition. * discriminate. + intuition. - cbn. destruct (A_eq_dec a a0); inversion H; subst. + subst. apply IHxs. rewrite H2. apply H2. + contradiction. Qed.
imports: Coq(Lia Lists.List) Equations(Equations)