fact: Parameter subterm_in_instantiated_term : forall p s t sigma, subterm_at_pos (apply_subst sigma t) p = Some s -> match subterm_at_pos t p with | Some u' => s = apply_subst sigma u' | None => exists v, exists q, exists q', p = q ++ q' /\ In v (var_list t) /\ subterm_at_pos t q = Some (Var v) /\ subterm_at_pos (apply_subst sigma (Var v)) q' = Some s end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)