proposition: Lemma Tins_le : forall (k : nat) (f g : TList) (d x : A), TIns x k f g -> forall n : nat, k <= n -> Tnth_def d f n = Tnth_def d g (S n).
proof: Proof. simple induction 1; auto with coc core arith datatypes. simple destruct n0; intros. inversion H2. simpl in |- *; auto with coc core arith datatypes. Qed.
imports: Arith MyList