PrintForm Definitions relation autom Sections AutomataTheory Doc

At: incl aux3 quo 1 2 1 2
1. n: {1...}
2. m: n
3. E: nnProp
4. EquivRel i,j:n. i E j
5. EquivRel i,j:m. i E j
6. x: i,j:m//(i E j)
7. y: i,j:m//(i E j)
8. x i,j:n//(i E j)

x = y i,j:n//(i E j) x = y i,j:m//(i E j)
By: Assert (y i,j:n//(i E j))
Generated subgoals:

1 y i,j:n//(i E j)
29. y i,j:n//(i E j)
x = y x = y i,j:m//(i E j)

About:
equalquotientnatural_numbermemberfunctionprop