proposition: Lemma IS_Min_supterm : forall f, IS R f -> exists g, IS (R @ supterm_eq) g /\ Min R g.
proof: Proof. intros f hf. set (Min' := fun f : nat -> NTM R => forall i x, subterm x (f i) -> forall g, g 0 = x -> ~IS R g). cut (exists g : nat -> NTM R, IS Rsup g /\ Min' g). intros [g [h1 h2]]. exists (fun i => g i). split_all. destruct (choice _ Rsup_left_total) as [next hnext]. set (a := min_NTM (NT_IS_elt 0 hf)). exists (iter a next). split. apply IS_iter. hyp. intros i x hx g g0 hg. destruct (iter a next i) as [t [[h [h0 hh]] ht]]. simpl in hx. ded (ht _ hx). absurd (NT R x). hyp. exists g. 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)