fact: Definition is_root_preserving (a : rule) := let (l,r) := a in match l, r with | Fun f _, Fun g _ => beq_symb f g | _, _ => true end.
imports: CoLoR(ATrs NatUtil LogicUtil ListUtil SN EqUtil VecUtil RelUtil BoundNat)