proposition: Lemma well_formed_replace_at_pos : forall p t u, well_formed t -> well_formed u -> well_formed (replace_at_pos t u p).
proof: Proof. intro p; induction p as [ | i p]; intros t u Wt Wu. simpl; assumption. destruct t as [ x | f l]. simpl; trivial. rewrite replace_at_pos_unfold. destruct (well_formed_unfold Wt) as [Wl L]; clear Wt. apply well_formed_fold; split. clear L; revert i; induction l as [ | t l]. intros; contradiction. intros i; case i; clear i. simpl; intros v [H | H]. subst v; apply IHp; trivial. apply Wl; left; apply eq_refl. apply Wl; right; assumption. simpl; intros i v [H | H]. subst v; apply Wl; left; apply eq_refl. apply IHl with i; trivial. intros; apply Wl; right; assumption. replace (length (replace_at_pos_list l u i p)) with (length l); trivial. clear; revert i; induction l as [ | t l]; simpl; trivial. intros [ | n]; simpl; trivial. rewrite <- IHl; trivial. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)