-(* congettura, come si fa? *)
-include "num/exadecim.ma".
-include "num/exadecim_lemmas.ma".
-
-nlemma decidable_ex_aux1 : ∀x.∀H:x0 = x.(x0 = x) ∨ (x0 ≠ x).
- #x; nelim x;
- ##[ ##1: #H; napply (or_introl … H)
- ##| ##*: #H; nelim (exadecim_destruct … H)
- ##]. nqed.
-
-nlemma decidable_ex0 : ∀x:exadecim.decidable (x0 = x).
- #x;
- nelim x;
- nnormalize;
- napply (Or_ind (x0=x) (x0≠x) ? ? …);
- ##[ ##1: napply (or_introl (x0 = x0) (x0 ≠ x0) (refl_eq …))
- ##| ##*:
-
- nnormalize;
- nelim x;
- ##[ ##1: nelim y;
- ##[ ##1: napply (or_introl (? = ?) (? ≠ ?) (refl_eq …))
- ##| ##*:
-
(*include "utility/utility.ma".
nlemma fold_right_neList2_aux3 :