fact: Parameter is_subterm_ok_true : forall s t, is_subterm s t = true -> {p : list nat | subterm_at_pos t p = Some s}.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)