proposition: Lemma maxvar_rules_init : forall R x, fold_left fold_max R x >= x.
proof: Proof. induction R; simpl; intros. refl. rewrite IHR. apply Nat.le_max_l. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)