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