At: fin alph list quo 1 1 1 1 1 2
1. Alph: Type
2. E: Alph*
Alph*Prop
3. n: 
4. f: nAlph
5. g: Alphn
6. InvFuns(n; Alph; f; g)
7. EquivRel x,y:Alph*. x E y
8. 
x,y:Alph*. Dec(x E y)
9. x: n*
10. y: n*
Dec(map(f;x) E map(f;y))
By: BackThru 8
Generated subgoals:None
About:
