fact: Parameter split_rel : forall R1 R2 s t, one_step (union _ R1 R2) t s <-> (one_step R1 t s \/ one_step R2 t s).
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec)