proposition: Lemma lab_rule_fval : forall v a n, n > maxvar_rule a -> lab_rule (fval v n) a = lab_rule v a.
proof: Proof. intros v [l r] n. simpl. rewrite gt_max. intuition. rewrite lab_fval. 2: hyp. rewrite lab_fval. 2: hyp. refl. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)