proposition: Lemma length_elemlist : forall (l : list A) (i : nat), i < length l -> length (elemlist l i) = 1.
proof: Proof. intros. unfold elemlist in |- *. rewrite length_trunc. trivial with arith. rewrite length_strip. inversion H. rewrite <- minus_Sn_m. auto with arith. auto with arith. rewrite <- minus_Sn_m. auto with arith. apply le_Sn_le. exact H1. apply lt_le_weak. exact H. Qed.
imports: Arith_compl Minus Lists_compl