proposition: Lemma wf_oi : well_founded ord_insert.
proof: Proof. cut (forall (n : nat) (l : list name), length l = n -> Acc ord_insert l). red in |- *; intros. apply H with (length a); auto with coc core arith datatypes. simple induction n. simple destruct l; intros. apply Acc_intro; intros. inversion_clear H0. inversion_clear H1. discriminate H. simple destruct l; simpl in |- *; intros. discriminate H0. injection H0; intros. apply Acc_intro; intros. inversion_clear H2. apply H. cut (S (length y) = length (n1 :: l0)); intros. simpl in H2. injection H2; auto with coc core arith datatypes. elim H1; auto with coc core arith datatypes. elim H3; auto with coc core arith datatypes. intros. simpl in |- *. elim H4; auto with coc core arith datatypes. Qed.
imports: Arith MyList MlTypes