proposition: Lemma gt_chain_min : forall f ts us v, Vrel1 (red R) ts us -> Vforall (SN (red R)) ts -> chain_min (Fun f us) v -> chain_min (Fun f ts) v.
proof: Proof. intros f ts us v gt_ts_us sn_ts chain_min_fus_v. unfold chain_min in chain_min_fus_v. destruct chain_min_fus_v as [chain_fus_v sn]. destruct sn as [esn_us esn_ts]. unfold chain_min. split. apply gt_chain with us; trivial. split. simpl. apply Vforall_lforall in sn_ts. trivial. trivial. Qed.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)