[Agda] no longer type checks

[Justus Matthiesen]

> Anyway, is there a simple workaround?

The following should do the job:

  bool-distinct : true ≡ false → ⊥
  bool-distinct ()

  is-in₀ : {X Y : Set} → X + Y → Bool
  is-in₀ (in₀ _) = true
  is-in₀ (in₁ _) = false

  lemma : {X Y : Set} {x : X} {y : Y} → in₀ x ≡ in₁ y → ⊥
  lemma e = bool-distinct (cong is-in₀ e)


Justus