proposition: Lemma gt_chain : forall f ts us v, Vrel1 (red R) ts us -> chain (Fun f us) v -> chain (Fun f ts) v.
proof: Proof. unfold chain, compose. intros. do 2 destruct H0. exists x. split. apply rt_trans with (y := Fun f us). apply rt_step. apply Vgt_prod_fun. exact H. exact H0. exact H1. Qed.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)