Kata

We can represent the suffix of a list with the following definition:

From Coq Require Import List.

Inductive suf {X : Type} : list X -> list X -> Prop :=
  | SInit (l : list X) : suf l l
  | SCons (x : X) (l l' : list X) (H : suf l l') : suf (x :: l) l'
.

open import Data.List public

data Suf {X : Set} : List X → List X → Set where
  sinit : ∀ l → Suf l l
  scons : ∀ x l l' → Suf l l' → Suf (x ∷ l) l'

Your task is to show that less is not more, aka forall X (x : X) (l : list X), ~ suf l (x :: l)..