#A #B #l #f elim l // #a #tl #Hind normalize //
qed.
-lemma lenght_rev_append: ∀A.∀l,acc:list A.
+lemma length_rev_append: ∀A.∀l,acc:list A.
|rev_append ? l acc| = |l|+|acc|.
#A #l elim l // #a #tl #Hind normalize
#acc >Hind normalize //
qed.
-lemma lenght_reverse: ∀A.∀l:list A.
+lemma length_reverse: ∀A.∀l:list A.
|reverse A l| = |l|.
// qed.
lemma split_len: ∀A,n,l. n ≤ |l| →
|\fst (split A l n)| = n.
#A #n #l #Hlen normalize >(eq_pair_fst_snd ?? (split_rev …))
-normalize >lenght_reverse >(split_rev_len … [ ] Hlen) normalize //
+normalize >length_reverse >(split_rev_len … [ ] Hlen) normalize //
qed.
lemma split_rev_eq: ∀A,n,l,acc. n ≤ |l| →