fact: Parameter replace_at_pos_is_replace_at_pos2 : forall t p u, subterm_at_pos t p = Some u -> replace_at_pos t u p = t.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)