proposition: Lemma item_trunc : forall (n : nat) (e : List) (t : A), item t e n -> exists f : List, trunc (S n) e f.
proof: Proof. simple induction n; intros. inversion_clear H. exists l; auto with coc core arith datatypes. inversion_clear H0. elim H with l t; intros; auto with coc core arith datatypes. exists x; auto with coc core arith datatypes. Qed.
imports: Le Gt List