PrintForm Definitions relation autom Sections AutomataTheory Doc

At: quotient of nsubn 1 1 1 1 1 1

1. E: 11Prop
2. EquivRel x,y:1. x E y
3. x,y:1. Dec(x E y)
4. 0 1

0 i,j:1//(i E j)

By: Inclusion 4

Generated subgoals:

None


About:
memberquotientnatural_numberfunctionpropall