fact: Definition status_union (f : M.symbol) : rpo.status_type := match f with | (true, f) => status_marked f | (_, f) => status f end.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)