proposition: Lemma red_NT A (R : rel A) t u : R t u -> NT R u -> NT R t.
proof: Proof. intros tu [f [f0 hf]]. subst. exists (fun k => match k with 0 => t | S k' => f k' end). intuition. intro k. destruct k. hyp. apply hf. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)