What I would do (caveat emptor, this is written off the top of my head):

Define a type for “paths” inside a formula:

```
Inductive path :=
| Root
| Left: path -> path
| Right: path -> path.
```

The representation is the obvious one, ie `Left (Left (Right Root))`

means “go left, go left, go right, you are there!”.

Valid paths in a given formula are supposed to point to a subterm, as per:

```
Inductive points: path -> formula -> formula -> Prop :=
| points_root: forall F, points Root F
| points_neg: forall P F H, points P F H -> points (Left P) (neg F) H
| points_conj_left: forall P F G H, points P F H -> points (Left P) (conj F G) H
| points_conj_right: forall P F G H, points P G H -> points (Right P) (conj F G) H
| (* etc *)
```

In words: `points P F G`

means that the path `P`

points to a subterm `G`

inside `F`

. A *valid path* `P`

relative a formula `F`

is one such that there exists `G`

such that `points P F G`

:

```
Definition valid (P : path) (F : formula) : Prop := exists G, points P F G.
```

One can use a path to retrieve the subterm it points to:

```
Fixpoint get (P : path) (F : formula) : option formula :=
match P, F with
| Root, F => Some F
| Left P, (neg F | equiv F | conj F _ | disj F _ | impl F _) => get P F
| Right P, (conj _ F | disj _ F | impl _ F) => get P F
| _ => None
end.
```

We should have the following equivalence:

```
Lemma points_get: forall P F G,
points P F G <-> get P F = Some G.
Admitted.
```

You can define a function `subst: path -> formula -> formula -> option formula`

:

```
Fixpoint subst (P : path) (F : formula) (G : formula) : option formula :=
match P, G with
| Root, _ => F
| Left P, neg G => neg (subst P F G)
| Left P, conj G H => conj (subst P F G) H
| Right P, conj G H => conj G (subst P F H)
| (* etc *)
| _ => None
end.
```

In words: `subst P F G`

is `Some H`

where `H`

is `G`

with the term pointed to by `P`

replaced by `F`

, if `P`

is valid in `G`

and `None`

otherwise.

This is made explicit by the following result:

```
Lemma valid_subst: forall P F G H,
valid P G -> subst P F G = Some H /\ points P H F.
Admitted.
```

Best wishes,

Nicolás