<div dir="ltr">I skipped some code in my previous mail, here is the complete version for those who are interested:<br><br>{-# OPTIONS --without-K --new-without-K #-}<br>-- Both flags are enabled for extra safety<br><br>module FinWithoutK where<br>

<br>open import Data.Empty<br>open import Data.Nat<br>open import Data.Product<br>open import Relation.Binary.PropositionalEquality<br><br>J : {A : Set} {x : A} (P : (y : A) → x ≡ y → Set) → <br>    P x refl → {y : A} → (q : x ≡ y) → P y q<br>

J P p refl = p<br><br>K : {A : Set} (x : A) → Set₁<br>K {A} x = (P : x ≡ x → Set) → P refl → (q : x ≡ x) → P q<br><br>proof-irrelevance : {A : Set} {x y : A} {e₀ : x ≡ y} → {{k : K x}} →<br>                    (P : x ≡ y → Set) → P e₀ → (e : x ≡ y) → P e<br>

proof-irrelevance {e₀ = refl} {{k}} P p e = k P p e<br><br>add-suc : {m n : ℕ} → m ≡ n → suc m ≡ suc n<br>add-suc refl = refl<br><br>drop-suc : {m n : ℕ} → suc m ≡ suc n → m ≡ n<br>drop-suc refl = refl<br><br>add-drop-lemma : {m n : ℕ} (q : suc m ≡ suc n) → add-suc (drop-suc q) ≡ q<br>

add-drop-lemma refl = refl<br><br>K-for-ℕ : {n : ℕ} → (P : n ≡ n → Set) → P refl → (q : n ≡ n) → P q<br>K-for-ℕ {zero} P p refl = p<br>K-for-ℕ {suc n} P p q = J (λ q _ → P q) aux (add-drop-lemma q) <br>  where<br>    aux : P (add-suc (drop-suc q))<br>

    aux = K-for-ℕ {n} (λ q → P (add-suc q)) p (drop-suc q)<br><br>data Fin : ℕ → Set where<br>  fz : {n : ℕ} → Fin (suc n)<br>  fs : {n : ℕ} → Fin n → Fin (suc n)<br><br>NoConfusion : {n : ℕ} (x : Fin n) {m : ℕ} (y : Fin m) → Set<br>

NoConfusion (fz {n})   (fz {m})   = n ≡ m<br>NoConfusion fz         (fs y)     = ⊥<br>NoConfusion (fs x)     fz         = ⊥<br>NoConfusion (fs {n} x) (fs {m} y) = Σ[ e ∈ n ≡ m ] subst Fin e x ≡ y<br><br>noConfusion : {n : ℕ} {x : Fin n} {m : ℕ} {y : Fin m} → <br>

              (e : n ≡ m) → subst Fin e x ≡ y → <br>              NoConfusion x y<br>noConfusion {x = fz}   refl refl = refl<br>noConfusion {x = fs x} refl refl = refl , refl<br><br>drop-fs : ∀ {o} (x y : Fin o) → fs x ≡ fs y → x ≡ y<br>

drop-fs x y q = proof-irrelevance {e₀ = e} (λ p → subst Fin p x ≡ y) x&#39;≡y refl<br>  where<br>    e = proj₁ (noConfusion refl q)<br>    x&#39;≡y = proj₂ (noConfusion refl q)<br><div><div class="gmail_extra"></div></div>

</div>