fact: Parameter subterm_subterm : forall t p s, subterm_at_pos t p = Some s -> (t=s) \/ (trans_clos direct_subterm s t).
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)