proposition: Lemma mon_apps_replace : forall u u', R u u' -> forall n (ts : Tes n) t i (h1 h2 : i<n), R (apps t (Vreplace ts h1 u)) (apps t (Vreplace ts h2 u')).
proof: Proof. intros u u' uu'. induction ts; intros t i h1 h2. lia. rename h into t0. simpl. destruct i; simpl. apply mon_apps_l. apply mon_app_r; auto. refl. apply IHts. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)