PrintForm Definitions relation autom Sections AutomataTheory Doc

At: quotient of nsubn 1 1 1 1 2 1
1. E: 11Prop
2. EquivRel x,y:1. x E y
3. x,y:1. Dec(x E y)
4. 0 i,j:1//(i E j)

InvFuns(1; i,j:1//(i E j); x.0; x.0)
By:
Unfold `inv_funs` 0
THEN
Analyze 0
Generated subgoals:

1 (x.0) o (x.0) = Id
2 (x.0) o (x.0) = Id

About:
natural_numberquotientlambdafunctionpropallmemberequal