proposition: Lemma deltabrel_add_var: forall i j n A s t m, deltabrel (add_var i j n A) s m t = deltabrel A s m t || eq_label_bool n m && (eq_state_bool i s && eq_state_bool j t).
proof: Proof. intros. destruct A. unfold deltabrel, deltafun, add_var, augment_var, statelabelmap_set_to_fun. simpl. repeat StateLabelMapProps.find_analyse; simpl; repeat (StateLabelMapProps.find_tac; sl_inject); bool_simpl; simpl; trivial. rewrite eqb_eq_nat_bool. apply orb_comm. num_analyse; nat_analyse; bool_simpl; trivial; subst; auto. elim H. apply StateLabel.eq_refl. num_analyse; nat_analyse; bool_simpl; trivial; subst; auto. elim H. apply StateLabel.eq_refl. rewrite eqb_eq_nat_bool. trivial. apply <-bool_prop_iff; bool_connectors; intuition. num_prop. nat_prop. subst. elim H2. apply StateLabel.eq_refl. apply <-bool_prop_iff; bool_connectors; intuition. num_prop. nat_prop. subst. elim H2. apply StateLabel.eq_refl. 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)