proposition: Lemma min_hd_red_dp : forall t u v, NT_min (red R) t -> hd_red R t u -> subterm_eq v u -> NT_min (red R) v -> hd_red (dp R) t v.
proof: Proof. intros t u v ht tu vu hv. redtac. subst. assert (hs : forall x, In x (vars l) -> ~NT (red R) (s x)). intros x vx nx. assert (hx : subterm (Var x) l). destruct (in_vars_subterm_eq vx) as [c hx]. destruct c. rewrite forallb_forall in hyp1. ded (hyp1 _ lr). rewrite hx in H. discr. exists (Cont f e t c t0). split_all. discr. ded (subterm_sub s hx). destruct ht as [ht1 ht2]. ded (ht2 _ H). contr. destruct (subterm_eq_sub_elim vu) as [w [hw1 hw2]]. destruct w. assert (hn : In n (vars l)). eapply hyp2. apply lr. eapply subterm_eq_vars. apply hw1. simpl. auto. destruct hv as [hv1 hv2]. absurd (NT (red R) v). rewrite <- SN_notNT_eq. eapply subterm_eq_sn. rewrite SN_notNT_eq. eapply hs. apply hn. hyp. hyp. subst. ex l (Fun f t) s. split_all. eapply dp_intro. apply lr. apply subterm_in_calls. 2: hyp. case_eq (defined f R); intro H. refl. destruct hv as [hv1 hv2]. absurd (NT (red R) (sub s (Fun f t))). 2: hyp. rewrite <- SN_notNT_eq. apply sn_args_sn_fun. hyp. hyp. apply Vforall_intro. intros a ha. rewrite SN_notNT_eq. apply hv2. apply subterm_fun. hyp. unfold negb_subterm. rewrite negb_ok. 2: apply bsubterm_ok. intro h. destruct ht as [ht1 ht2]. absurd (NT (red R) (sub s (Fun f t))). apply ht2. apply subterm_sub. hyp. destruct hv as [hv1 hv2]. hyp. Qed.
imports: Coq(IndefiniteDescription ClassicalChoice ProofIrrelevance Lia) CoLoR(RelUtil ATrs LogicUtil ACalls SN InfSeq LeastNat ListUtil BoundNat NatUtil VecUtil ADP NotSN_IS ASN BoolUtil ClassicUtil)