What would be the ZDD approach in Prolog that also provides quantifiers.

Notation for existential quantifier would be as follows:

```
X^F
```

where X is the bound variable and F is the formula. It corresponds

to the following formula:

```
F[X/0] v F[X/1]
```

How would one go about and write a Prolog routine that takes a ZDD

for F and a variable X and produces the ZDD for X^F ?

P.S.: Cross posted on stackoverflow. https://\stackoverflow.com/q/64959919/502187

But I am not sure whether Kuniaki Mukai visits stackoverflow.