proposition: Lemma map_lab_rule_fval : forall v R n, n > maxvar_rules R -> map (lab_rule (fval v n)) R = map (lab_rule v) R.
proof: Proof. induction R; simpl; intros. refl. unfold maxvar_rules in H. simpl in H. rewrite lab_rule_fval, IHR. refl. apply Nat.le_lt_trans with (fold_left fold_max R (fold_max 0 a)). apply maxvar_rules_init_mon. apply Nat.le_max_l. hyp. apply Nat.le_lt_trans with (fold_left fold_max R (fold_max 0 a)). apply maxvar_rules_init. hyp. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)