proposition: Lemma example: same_relation _ (clos_refl_trans _ (union _ R S)) (comp (clos_refl_trans _ R) (clos_refl_trans _ (comp S (clos_refl_trans _ R)))).
proof: Proof. intros. fold_relAlg A. kleene_reflexivity. Qed.
imports: ATBR(ATBR)