あぐだちゃんがトリックを仕掛けて来たようです

data Bool : Set0 where
  true : Bool ; false : Bool

data _∨_ (A : Set0) (B : Set0) : Set0 where
  intro1 : A -> A ∨ B
  intro2 : B -> A ∨ B

data Id {A : Set0} : A -> A -> Set0 where
  refl : (a : A) -> Id a a

-- Boolはなぁ・・・trueか、falseだけなんだよォォォッ！！
lemma : (b : Bool) -> (Id b true) ∨ (Id b false)
lemma b with b
... | true = intro1 (refl b)
... | false =  intro2 (refl false) -- これは出来る

{-
エラーメッセージ
b != true of type Bool
when checking that the expression intro1 (refl b) has type
Id true true ∨ Id true false

Id true true ∨ Id true false
には落とせるのに、b != trueとか言われても困っちゃうわ...
-}

{-
lemma : (b : Bool) -> (Id b true) ∨ (Id b false)
lemma true = intro1 (refl true)
lemma false = intro2 (refl false)

これは勿論大丈夫
-}

どうしてこうなった...?