Forall Question

[Troy Pocklington]

So if we have something like the following:

(forall v : t)

can we just say expansion of forall and basic tautology to say it is equivalent to t?

--
-Troy

[David Rager]

Here you go:

(forall v : t)

<--> { Taut: short circuit }

(implies t (forall v : t))

<--> { Universal conclusion }

(implies t t)

<--> { Taut: short-circuit }

t


Actually, since you can factor the goal into (implies t (forall v :
t)), you should be able to just use universal conclusion directly.
This is step 1 of the formal definition of Rule of Inference:
Universal Conclusion on page 122.

(forall v : t)

<--> { Universal conclusion }

t