proposition: Lemma NT_min_intro : exists u, subterm_eq u t /\ NT_min R u.
proof: Proof. set (P := fun n => exists u, subterm_eq u t /\ size u = n /\ NT R u). assert (exP : exists n, P n). ex (size t) t. split_all. refl. destruct (ch_min exP) as [n [[Pn nleP] nmin]]. destruct Pn as [u [ut [un hu]]]. subst n. exists u. unfold NT_min, min. split_all. rename u0 into v. assert (size u <= size v). apply nleP. exists v. split_all. eapply subterm_eq_trans. apply subterm_strict. apply H. hyp. ded (subterm_size H). lia. 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)