proposition: Lemma acc_subterms_pi : forall pi v1 v2 R, (forall x t, ~ (R t (Var x))) -> is_primary_pi pi R -> forall l, (forall t, In t l -> Acc (one_step (@union _ R (Pi pi v1 v2))) t) -> Acc (one_step (@union _ R (Pi pi v1 v2))) (Term pi l).
proof: Proof. intros pi x1 x2 R R_var P l Hl; assert (Acc_l : Acc (one_step_list (one_step (@union _ R (Pi pi x1 x2)))) l). rewrite <- acc_one_step_list; trivial. generalize Hl; clear Hl; induction Acc_l as [l Acc_l IH]. intros Acc_l'; apply Acc_intro. intros t H; inversion H; clear H; subst. inversion H0; clear H0; subst. destruct t2 as [v2 | f2 l2]. absurd ((@union _ R (Pi pi x1 x2)) t1 (Var v2)); trivial. intros [H' | HPi]. apply (R_var _ _ H'). inversion HPi. simpl in H; injection H; clear H; intros; subst. destruct H2 as [H2 | Hpi]. destruct (P t1 (Term pi l2) H2 pi) as [_ F]; simpl in F. apply False_rect; apply F. generalize (F.Symb.eq_bool_ok pi pi); case (F.Symb.eq_bool pi pi). trivial. intro pi_diff_pi; absurd (pi =pi); trivial. trivial. assert (t1_in_ll : In (apply_subst sigma t1) (map (apply_subst sigma) l2)). inversion Hpi; subst; simpl; [left | right; left]; trivial. apply Acc_l'; trivial. apply IH; trivial. generalize l H2 Acc_l'; clear l H2 Acc_l' Acc_l IH. intros l H; induction H. intros Acc_l t [t_eq_t1 | t_in_l]. subst; assert (Acc_t2 := Acc_l t2 (or_introl _ (eq_refl _))). inversion Acc_t2. apply H0; trivial. apply Acc_l; right; trivial. intros Acc_l2 u [u_eq_t | u_in_l1]. subst; apply Acc_l2; left; trivial. apply IHone_step_list; trivial. intros; apply Acc_l2; right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)