proposition: Lemma maxvar_rules_elim : forall a R n, In a R -> n > maxvar_rules R -> n > maxvar_rule a.
proof: Proof. unfold maxvar_rules. induction R; simpl; split_all. subst. unfold fold_max in H0. simpl in H0. fold fold_max in H0. apply Nat.le_lt_trans with (fold_left fold_max R (fold_max 0 a)). apply maxvar_rules_init. hyp. apply IHR. hyp. apply Nat.le_lt_trans with (fold_left fold_max R (fold_max 0 a0)). apply maxvar_rules_init_mon. apply Nat.le_max_l. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)