+definition enumn ≝ λn.enumnaux n n (le_n n).
+
+definition Nat_to ≝ λn. DeqSig DeqNat (λi.i<n).
+
+(* lemma prova : ∀n. carr (Nat_to n) = (Σx.x<n). // *)
+
+lemma memb_enumn: ∀m,n,i:DeqNat. ∀h:n ≤ m. ∀k: i < m. n ≤ i →
+ (¬ (memb (Nat_to m) (mk_Sig ?? i k) (enumnaux n m h))) = true.
+#m #n elim n -n // #n #Hind #i #ltm #k #ltni @sym_eq @noteq_to_eqnot @sym_not_eq
+% #H cases (orb_true_l … H)
+ [#H1 @(absurd … (\P H1)) % #Hfalse
+ cut (∀A,P,a,a1,h,h1.mk_Sig A P a h = mk_Sig A P a1 h1 → a = a1)
+ [#A #P #a #a1 #h #h1 #H destruct (H) %] #Hcut
+ lapply (Hcut nat (λi.i<m) i n ? ? Hfalse) #Hfalse @(absurd … ltni)
+ @le_to_not_lt >Hfalse @le_n
+ |<(notb_notb (memb …)) >Hind normalize /2/
+ ]
+qed.
+
+
+lemma enumn_unique_aux: ∀n,m. ∀h:n ≤ m. uniqueb (Nat_to m) (enumnaux n m h) = true.
+#n elim n -n // #n #Hind #m #h @true_to_andb_true // @memb_enumn //
+qed.
+
+lemma enumn_unique: ∀n.uniqueb (Nat_to n) (enumn n) = true.
+#n @enumn_unique_aux
+qed.
+
+(* definition ltb ≝ λn,m.leb (S n) m. *)
+lemma enumn_complete_aux: ∀n,m,i.∀h:n ≤m.∀k:i<m.i<n →
+ memb (Nat_to m) (mk_Sig ?? i k) (enumnaux n m h) = true.
+#n elim n -n
+ [normalize #n #i #_ #_ #Hfalse @False_ind /2/
+ |#n #Hind #m #i #h #k #lein whd in ⊢ (??%?);
+ cases (le_to_or_lt_eq … (le_S_S_to_le … lein))
+ [#ltin cut (eqb (Nat_to m) (mk_Sig ?? i k) (mk_Sig ?? n h) = false)
+ [normalize @not_eq_to_eqb_false @lt_to_not_eq @ltin]
+ #Hcut >Hcut @Hind //
+ |#eqin cut (eqb (Nat_to m) (mk_Sig ?? i k) (mk_Sig ?? n h) = true)
+ [normalize @eq_to_eqb_true //
+ |#Hcut >Hcut %
+ ]
+ ]