proof - CoNat : 0 が左に中立であることを証明する

Question

Jesper Cockx と Andreas Abel によるこの論文CoNatから引用した の定義を試しています。

open import Data.Bool
open import Relation.Binary.PropositionalEquality

record CoNat : Set where
  coinductive
  field iszero : Bool
        pred : .(iszero ≡ false) -> CoNat

open CoNat public

私は定義zeroし、plus：

zero : CoNat
iszero zero = true
pred zero ()

plus : CoNat -> CoNat -> CoNat
iszero (plus m n)                                  = iszero m ∧ iszero n
pred (plus m n) _ with iszero m | inspect iszero m | iszero n | inspect iszero n
...                | false | [ p ] | _     | _     = plus (pred m p) n
...                | true  | _     | false | [ p ] = plus m (pred n p)
pred (plus _ _) () | true  | _     | true  | _

そして、私は二相似性を定義します:

record _≈_ (m n : CoNat) : Set where
  coinductive
  field
    iszero-≈ : iszero m ≡ iszero n
    pred-≈ : ∀ p q -> pred m p ≈ pred n q

open _≈_ public

しかし、私は と似ている証明に行き詰まっていplus zero nますn。私の推測では、証明には (少なくとも) with-clause for が必要ですiszero n:

plus-zero-l : ∀ n -> plus zero n ≈ n
iszero-≈ (plus-zero-l _)   = refl
pred-≈ (plus-zero-l n) p q with iszero n
... | _ = ?

しかし、Agda は次のエラー メッセージに対して不平を言っています。

iszero n != w of type Bool
when checking that the type
(n : CoNat) (w : Bool) (p q : w ≡ false) →
(pred (plus zero n) _ | true | [ refl ] | w | [ refl ]) ≈ pred n _
of the generated with function is well-formed

この証明はどうすればできますか？