### Coq

At this moment I am just trying to run the code in the Coq Tutorial...

The following e-script, corresponding to the section "Existential Quantification" of the tutorial, is not working as it should:

 ```*;; (find-coqv81w3m "tutorial.html#htoc12" "Sections and signatures") * (eepitch-coqtop) * (eepitch-kill) * (eepitch-coqtop) Reset Initial. Section Predicate_calculus. Variable D : Set. Variable R : D -> D -> Prop. Section R_sym_trans. Hypothesis R_symmetric : forall x y:D, R x y -> R y x. Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z. Lemma refl_if : forall x:D, (exists y, R x y) -> R x x. Check ex. intros x x_Rlinked. intro y. ```

Here is its log:

```Welcome to Coq 8.1pl3 (Dec. 2007)

Coq < Reset Initial.

Coq < Section Predicate_calculus.

Coq < Variable D : Set.
D is assumed

Coq < Variable R : D -> D -> Prop.
R is assumed

Coq < Section R_sym_trans.

Coq < Hypothesis R_symmetric : forall x y:D, R x y -> R y x.
R_symmetric is assumed

Coq < Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z.
R_transitive is assumed

Coq < Lemma refl_if : forall x:D, (exists y, R x y) -> R x x.
1 subgoal

D : Set
R : D -> D -> Prop
R_symmetric : forall x y : D, R x y -> R y x
R_transitive : forall x y z : D, R x y -> R y z -> R x z
============================
forall x : D, (exists y : D, R x y) -> R x x

refl_if < Check ex.
ex
: forall A : Type, (A -> Prop) -> Prop

1 subgoal

D : Set
R : D -> D -> Prop
R_symmetric : forall x y : D, R x y -> R y x
R_transitive : forall x y z : D, R x y -> R y z -> R x z
x : D
x_Rlinked : exists y : D, R x y
============================
R x x

refl_if < intro y.
Toplevel input, characters 0-7
> intro y.
> ^^^^^^^
User error: No product even after head-reduction

refl_if <
```