PrintForm
Definitions
choice
1
Sections
AutomataTheory
Doc
At:
equiv
rel
fun
1
1.
T:
Type
2.
E:
T
T
3.
s:
T
4.
t:
T
5.
EquivRel x,y:T. x E y
6.
s E t
7.
x:
T
E(s,x) = E(t,x)
By:
BackThru
Thm*
a,b:
. (a
b)
a = b
Generated subgoal:
1
E(s,x)
E(t,x)
About:
T
E(s,x) = E(t,x)
a,b:. (a 
b) 
a = b
