proposition: Lemma subs1_rel_mon_preorder R : PreOrder R -> Monotone R -> forall u s s', subs_rel R (fv u) s s' -> R (subs1 s u) (subs1 s' u).
proof: Proof. intros R_qo R_mon. induction u; simpl; intros s s' h. apply h; simpl. set_iff. refl. refl. destruct R_mon. rewrite IHu1 with (s:=s) (s':=s'), IHu2 with (s:=s) (s':=s'). refl. intros x hx. apply h. simpl. apply union_subset_2. hyp. intros x hx. apply h. simpl. apply union_subset_1. hyp. mon. apply IHu. intros y hy. unfold Def.update. eq_dec y x. refl. apply h. set_iff. auto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)