proposition: Lemma subterm_eq_min_term : subterm_eq min_term t.
proof: Proof. unfold min_term. destruct (constructive_indefinite_description (fun u : term => subterm_eq u t /\ NT_min R u) NT_min_intro) as [u hu]. simpl. tauto. 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)