proposition: Lemma I_mon : forall f, Vmonotone1 (fint I f) Dge.
proof: Proof. unfold Vmonotone1, Vmonotone, Vmonotone_i, RelUtil.monotone. intros. rewrite H0. refl. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)