PrintForm Definitions choice 1 Sections AutomataTheory Doc

At: equiv rel fun 1 1 1 1 2
1. T: Type
2. E: TT
3. s: T
4. t: T
5. Refl(T;x,y.x E y)
6. a,b:T. (a E b) (b E a)
7. a,b,c:T. (a E b) (b E c) (a E c)
8. s E t
9. x: T
10. E(t,x)

E(s,x)
By: FwdThru 7 [8;10]
Generated subgoals:

None

About:
assertapplyuniversefunctionboolallimplies