+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 %
+ ]
+ ]