proposition: Lemma wf_on_mul_rest : well_founded rpo_mul_rest.
proof: Proof. apply wf_incl with (clos_trans _ rpo_mul_rest_step). apply rpo_mul_trans_clos. apply wf_clos_trans. unfold well_founded; intro a; induction a. apply Acc_intro; intros m H; inversion_clear H. generalize (list_permut_length H1); intro Abs; simpl in Abs; absurd (0 = S (length (map tt (a :: lc)))); trivial; discriminate. generalize a0 IHa; clear a0 IHa; pattern a; refine (well_founded_ind wf_on_rest _ _ a); clear a. intros; apply (Acc_iter (R:= rpo_rest) (fun a => Acc rpo_rest a -> forall m, Acc rpo_mul_rest_step m -> Acc rpo_mul_rest_step (a :: m))); trivial. destruct x; rename tt0 into s; rename sn0 into Acc_s; clear a0 IHa; intros b IH Acc_b m Acc_m. apply (Acc_iter (R:= rpo_mul_rest_step) (fun m => Acc rpo_mul_rest_step m -> Acc rpo_mul_rest_step (b :: m))); trivial. clear m Acc_m; intros m IHm Acc_m; apply Acc_intro. intros y lt_y; elim (two_cases_rpo _ _ _ lt_y); clear lt_y; intro lt_y. elim lt_y; clear lt_y; intros n' H'; elim H'; clear H'; intros P M; apply list_permut_map_acc with (b :: n'). apply list_permut_sym; trivial. apply IHm; trivial; apply Acc_inv with m; trivial. elim lt_y; clear lt_y; intros k H'; elim H'; clear H'; intros M P; apply list_permut_map_acc with (k ++ m). apply list_permut_sym; trivial. clear P; induction k; trivial. simpl; apply IH. apply M; left; trivial. apply Acc_inv with b; trivial; apply M; left; trivial. apply IHk; intros; apply M; right; trivial. apply wf_on_rest. apply wf_on_rest. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term