proposition: Lemma is_primary_pi_not_subrule: forall (R:relation term) pi (Hpi:is_primary_pi pi R) t1 t2 p l, R t2 t1 -> subterm_at_pos t2 p = Some (Term pi l) -> False.
proof: Proof. intros R pi Hpi t1 t2 p l H H0. unfold is_primary_pi in Hpi. destruct (Hpi _ _ H pi) as [ F _]. elim F;trivial. clear - H0. revert t2 H0. induction p. intros t2 H2. simpl in H2. injection H2;clear H2;intros;subst t2. simpl. generalize (F.Symb.eq_bool_ok pi pi); case ( F.Symb.eq_bool pi pi);trivial. intro abs;elim abs;trivial. intros t2 H2;simpl in H2. destruct t2. discriminate H2. case_eq (nth_error l0 a);intros. rewrite H in H2. simpl. generalize (F.Symb.eq_bool_ok pi a0); case ( F.Symb.eq_bool pi a0);trivial. intros. revert a H. induction l0. intros a H;destruct a; simpl in H; discriminate. intros a' H;destruct a'. simpl in *. injection H;intros;subst. rewrite IHp. trivial. assumption. simpl in *. rewrite (IHl0 a');trivial. auto with *. rewrite H in H2;discriminate. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)