I am trying to solve a rather simple proof goal with a ML tactic. My goal has the form:

```
⋀x f1 f2 g1 g2. (⋀z1. z1 ∈ set1_sum2 x ⟹ f1 z1 = g1 z1) ⟹ (⋀z2. z2 ∈ set2_sum2 x ⟹ f2 z2 = g2 z2) ⟹ map_sum2 f1 f2 x = map_sum2 g1 g2 x
```

and I have a theorem of the form

```
(⋀z1. z1 ∈ set1_sum2 ?x ⟹ ?f1.0 z1 = ?g1.0 z1) ⟹ (⋀z2. z2 ∈ set2_sum2 ?x ⟹ ?f2.0 z2 = ?g2.0 z2) ⟹ map_sum2 ?f1.0 ?f2.0 ?x = map_sum2 ?g1.0 ?g2.0 ?x
```

So I need to instanciate the schematic variables of the theorem with the forall bound variables of the goal. I can get the bound variables with `Subgoal.SUBPROOF`

, but I have no idea what the ML equivalent of the lowercase `of`

is

Last updated: Jul 15 2022 at 23:21 UTC