fact: Axiom subst_comp_is_subst_comp_aux1 : forall v sigma f, find eq_variable_dec v (map_subst f sigma) = match find eq_variable_dec v sigma with | None => None | Some t => Some (f v t) end.
imports: List more_list list_permut list_set Arith