proposition: Lemma labelling_add_var : forall n A i j s t c, labelling n (fun a => deltabrel (add_var s t c A) i a j) == labelling n (fun a => deltabrel A i a j) + xif (eq_state_bool s i && eq_state_bool t j && leb (S c) n) (RegExp.var c: regex) 0.
proof: Proof. intros. induction n. unfold labelling. bool_simpl. simpl. fold_regex. semiring_reflexivity. rewrite 2 labelling_S. rewrite IHn. clear IHn. rewrite deltabrel_add_var. bool_simpl. unfold labelling; simpl. num_analyse; try num_lia_false; subst; simpl; bool_simpl; simpl; fold_regex; try semiring_reflexivity. case (deltabrel A i (num_of_nat n) j); simpl; fold_regex; semiring_reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(DKA_CheckLabels) ATBR(StrictStarForm) ATBR(Utils_WF) Coq(Relations)