created Head to ask for help

src/extra/Head.agda

@@ -0,0 +1,40 @@
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.List using (List; []; _∷_; dropWhile)
+open import Data.Char using (Char)
+open import Data.Bool using (Bool; true; false)
+import Data.Char as Char using (_≟_)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Nullary.Decidable using (⌊_⌋)
+
+
+data Head {A : Set} (P : A → Bool) : List A → Set where
+  head : ∀ (c : A) (s : List A) → P c ≡ true → Head P (c ∷ s)
+
+prime : Char
+prime = '′'
+
+isPrime : Char → Bool
+isPrime c = ⌊ c Char.≟ prime ⌋
+
+head-lemma : ∀ (s : List Char) → ¬ Head isPrime (dropWhile isPrime s)
+head-lemma [] = λ()
+head-lemma (c ∷ s) with isPrime c 
+...                   | true       =  head-lemma s
+...                   | false      =  ¬h
+  where
+  ¬h : ¬ Head isPrime (c ∷ s)
+  ¬h (head c s eqn′) = {!!}
+
+{-
+Goal: ⊥
+————————————————————————————————————————————————————————————
+s    : List Char
+c    : Char
+eqn′ : ⌊ (c Char.≟ '′' | .Agda.Builtin.Char.primCharEquality c '′')
+       ⌋
+       ≡ true
+s    : List Char
+c    : Char
+-}