PrintForm Definitions relation autom Sections AutomataTheory Doc

At: incl aux5 quo 1 1 1
1. T: Type
2. E: TTProp
3. a:T. a E a
4. Sym x,y:T. x E y & Trans x,y:T. x E y
5. x: T
6. y: T
7. x = y

x E y
By: InstHyp [x] 3
Generated subgoal:

18. x E x
x E y

About:
universefunctionpropallandequal