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 …))
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 …))
qed.
lemma split_rev_eq: ∀A,n,l,acc. n ≤ |l| →
qed.
lemma split_rev_eq: ∀A,n,l,acc. n ≤ |l| →