proposition: Lemma well_formed_subterm : forall t p s, well_formed t -> subterm_at_pos t p = Some s -> well_formed s.
proof: Proof. fix well_formed_subterm 2; intros t p; case p; clear p. intros s Wt Sub; injection Sub; intros; subst; assumption. intros i p s; simpl; case t; clear t. intros; discriminate. intros f l Wt Sub; case_eq (nth_error l i); [intros ti F | intros F]; rewrite F in Sub. apply (well_formed_subterm ti p). apply (proj1 (well_formed_unfold Wt)). destruct (nth_error_ok_in i l F) as [l' [l'' [_ H]]]; subst l; apply in_or_app; right; left; reflexivity. assumption. discriminate. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)