proposition: Lemma Rdp_left_total : forall t, exists u, Rdp t u.
proof: Proof. intros [t [[f [h0 hf]] ht]]. subst. destruct (classic (IS (int_red R) f)). destruct (NT_int_red_subterm_NT_red H). ded (ht x). intuition. unfold IS in H. rewrite not_forall_eq in H. set (k := proj1_sig (ch_min H)). assert (hk : hd_red R (f k) (f (S k))). ded (hf k). destruct (red_split H0). hyp. ded (ch_minP _ H). contr. assert (hk' : int_red R # (f 0) (f k)). cut (forall i, i <= k -> int_red R # (f 0) (f i)). intro h. apply h. refl. induction i; intro hi. apply rt_refl. apply rt_trans with (f i). apply IHi. lia. apply rt_step. apply NNPP. intro h. assert (k <= i). apply is_min_ch. hyp. lia. assert (NT_min (red R) (f k)). split. exists (fun i => f (i+k)). intuition. intro i. apply hf. eapply int_red_rtc_min. apply hk'. hyp. assert (NT (red R) (f (S k))). apply NT_IS_elt. hyp. exists (min_NTM H1). exists (mkNTM H0). simpl. intuition. eapply min_hd_red_dp. hyp. apply hk. apply subterm_eq_min_term. apply NT_min_term. 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)