直観論理では排中律は成り立たないし, 特に一般の型について \[\forall a,b,~ a = b \lor a \ne b\] は成立しない.

けど、`a`

`b`

に具体的な型が与えられていて, それが普通日常で考える常識的なモノであれば, これは普通の成り立つ.

```
(*
Excluded Middle Law (EML) of concrete types
*)
Theorem eml_bool : forall a b : bool, a = b \/ a <> b.
Proof.
case; case; (by left) + (by right).
Qed.
Theorem eml_nat : forall a b : nat, a = b \/ a <> b.
Proof.
induction a as [|a' IHa].
case. by left. by right.
case. by right.
intro b'.
move: (IHa b').
case.
- by left; apply f_equal.
- by right; injection.
Qed.
Theorem eml_nat_list : forall (a b : list nat), a = b \/ a <> b.
Proof.
induction a as [|x xs IH].
case. by left. by right.
case. by right.
move => y ys.
move: (IH ys); case => [E|E]; move: (eml_nat x y); case => [F|F];
(rewrite E; rewrite F; by left) + (by right; injection).
Qed.
```