[\lambda z:nat. \lambda h:(le O z). (eq nat O O)]
match (le_n O): le with
[ le_n \Rightarrow (refl_equal nat O)
| (le_S x y) \Rightarrow (refl_equal nat O) ]
###### INTERPRETATION NUMBER 1 ######
### (* disambiguation environment  *)
alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1
alias id eq = cic:/Coq/Init/Logic/eq.ind#1/1
alias id le = cic:/Coq/Init/Peano/le.ind#1/1
alias id le_n = cic:/Coq/Init/Peano/le.ind#1/1/1
alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
alias id refl_equal = cic:/Coq/Init/Logic/eq.ind#1/1/1
### (* METASENV after disambiguation  *)

### (* TERM after disambiguation      *)

<[z:nat][h:(le O z)](eq nat O O)>Cases (le_n O) of 
 le_n => (refl_equal nat O)
 le_S => [x:nat][y:(le O x)](refl_equal nat O)
end
### (* TYPE_OF the disambiguated term *)
([z:nat][h:(le O z)](eq nat O O) O (le_n O))
### (* REDUCED disambiguated term     *)
(refl_equal nat O)