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