proposition: Lemma Tins_gt : 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 n.
proof: Proof. simple induction 1; auto with coc core arith datatypes. intros. inversion_clear H0. simple destruct n0; intros. auto with coc core arith datatypes. simpl in |- *; auto with coc core arith datatypes. Qed.
imports: Arith MyList