proposition: Lemma Rsup_left_total : forall t, exists u, Rsup t u.
proof: Proof. intros [t [[f [h0 hf]] ht]]. exists (min_NTM (NT_IS_elt 1 hf)). unfold Rsup. simpl. exists (f 1). subst t. split_all. apply subterm_eq_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)