fact: Axiom subterm_at_pos_apply_subst_apply_subst_subterm_at_pos : forall t p sigma, match subterm_at_pos t p with | Some u => subterm_at_pos (apply_subst sigma t) p = Some (apply_subst sigma u) | None => True end.
imports: List more_list list_permut list_set Arith