-- A solution for A5.1 of the current GLoIn assignment sheet
open import Data.Nat
open import Data.Nat.Tactic.RingSolver using (solve-∀)
open import Relation.Binary.PropositionalEquality using (_≡_ ; subst)


module _ (A B : Set) where
  postulate pierce : ((A → B) → A) → A

  ϕ : ℕ → Set
  ϕ zero = A → B
  ϕ (suc n) = ϕ n → A

  helper : ∀ n → n + suc (n + zero) + 2 ≡ suc (n + (n + zero) + 2)
  helper = solve-∀

  lemma : ∀ (n : ℕ) → ϕ(2 * n + 2)
  lemma zero = pierce
  lemma (suc n) H = (subst ϕ (helper n) H) (lemma n)