proposition: Lemma is_a_pos_exists_subtem : forall t p, is_a_pos t p = true -> exists u, subterm_at_pos t p = Some u.
proof: Proof. intros t p; generalize t; clear t; induction p as [ | i q ]. intros t _; exists t; trivial. intros t; destruct t as [ x | f l ]; simpl. intros; discriminate. destruct (nth_error l i) as [ ti | ]. intro; apply IHq; trivial. intros; discriminate. Qed.
imports: List more_list list_permut list_set Arith