-(*
-lemma nth_make : ∀A,i,n,j,a,d. i < n → nth i ? (make_veci A a n j) d = a (j+i).
-#A #i elim i
- [#n #j #a #d #ltOn @(lt_O_n_elim … ltOn) <plus_n_O //
- |#m #Hind #n #j #a #d #Hlt lapply Hlt @(lt_O_n_elim … (ltn_to_ltO … Hlt))
- #p <plus_n_Sm #ltmp @Hind @le_S_S_to_le //
- ]
-qed. *)
-
-(*
-lemma mk_config_eq_s: ∀S,sig,s1,s2,t1,t2.
- mk_config S sig s1 t1 = mk_config S sig s2 t2 → s1=s2.
-#S #sig #s1 #s2 #t1 #t2 #H destruct //
-qed.
-
-lemma mk_config_eq_t: ∀S,sig,s1,s2,t1,t2.
- mk_config S sig s1 t1 = mk_config S sig s2 t2 → s1=s2.
-#S #sig #s1 #s2 #t1 #t2 #H destruct //
-qed.
-*)
-