Universal quantification is a general expression about *everything* (`Forall`

: $\forall$).

The `Forall`

**Expression** derives from `proveit.OperationOverInstances`

. As such, it has instance variables (`instance_vars`

) with an instance expression (`instance_expr`

) and may be restricted to a `domain`

and have zero or more `conditions`

. For example $\forall_{x, y \in S~|~Q(x),~R(x, y)} P(x, y)$ means that $P(x, y)$ is `TRUE`

for all occurrences of $x$ and $y$ in domain $S$ given that the conditions $Q(x)$ and $R(x, y)$ are satisfied. The `conditions`

may be any **Expression**s involving the instance variables.

In [1]:

```
import proveit
%theory
```