-lemma vector_nil: ∀A.∀v:Vector A 0.
- v = mk_Vector A 0 (nil A) (refl ??).
-#A * * // #a #tl normalize #H destruct
-qed.
-
-lemma nth_default : ∀A,i,n.∀v:Vector A n.∀d1,d2. i < n →
- nth i ? v d1 = nth i ? v d2.
-#A #i elim i -i
- [#n #v #d1 #d2 #ltOn lapply v @(lt_O_n_elim … ltOn)
- -v #m #v >(vec_expand … v) //
- |#i #Hind #n #v #d1 #d2 #ltn lapply ltn lapply v @(lt_O_n_elim … (ltn_to_ltO … ltn))
- -v -ltn #m #v #ltim >(vec_expand … v) @(Hind m (vec_tail A (S m) v) d1 d2 ?)
- @le_S_S_to_le //
- ]
-qed.
-
-lemma eq_vec: ∀A,n.∀v1,v2:Vector A n.∀d.
- (∀i. i < n → nth i A v1 d = nth i A v2 d) → v1 = v2.
-#A #n elim n -n
- [#v1 #v2 #H >(vector_nil A v1) >(vector_nil A v2) //
- |#n #Hind #v1 #v2 #d #H >(vec_expand … v1) >(vec_expand … v2)
- >(Hind (vec_tail … v1) (vec_tail … v2) d)
- [cut (vec_hd A n v1 = vec_hd A n v2) //
- cut (∀i,d1,d2. i < S n → nth i A v1 d1 = nth i A v2 d2)
- [#i #d1 #d2 #Hi >(nth_default ????? d) // >(nth_default ???? d2 d) // @H //]
- -H #H @(H 0) //
- |#i #ltin @(H (S i)) @le_S_S //
- ]
- ]
-qed.
-