proposition: Lemma is_a_pos_exists_subterm : forall t p, is_a_pos t p = true <-> exists u, subterm_at_pos t p = Some u.
proof: Proof. intros t p; revert t; induction p as [ | i q ]. intros t; split. intros _; exists t; trivial. intros _; trivial. intros t; destruct t as [ x | f l ]; simpl; split. intros; discriminate. intros [u Abs]; discriminate. destruct (nth_error l i) as [ ti | ]. intro; rewrite <- IHq; trivial. intros; discriminate. intros [u Sub]; destruct (nth_error l i). rewrite IHq; exists u; trivial. discriminate. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)