proposition: Lemma ins_le : forall (k : nat) (f g : List) (d x : A), insert x k f g -> forall n : nat, k <= n -> nth_def d f n = nth_def d g (S n).
proof: Proof. simple induction 1; auto with coc core arith datatypes. simple destruct n0; intros. inversion_clear H2. simpl in |- *. auto with coc core arith datatypes. Qed.
imports: Le Gt List