fact: Definition well_formed_subst sigma := forall v, match find eq_var_bool v sigma with | None => True | Some t => well_formed t end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)