I'm trying out Coq, but I'm not completely sure what I'm doing. Is:

```
Theorem new_theorem : forall x, P:Prop /\ Q:Prop
```

Equivalent to:

```
∀x ( P(x) and Q(x) )
```

Edit: I think they are.

Skip to content
# R – How to write ∀x ( P(x) and Q(x) ) in Coq

###### Related Question

coqlogicpredicateproof

I'm trying out Coq, but I'm not completely sure what I'm doing. Is:

```
Theorem new_theorem : forall x, P:Prop /\ Q:Prop
```

Equivalent to:

```
∀x ( P(x) and Q(x) )
```

Edit: I think they are.

## Best Solution

Are you having problems with the syntax?