At: fin alph list quo 1 1 1 1 1 3 1 1 1 1 2 1 1
1. Alph: Type
2. E: Alph*
Alph*Prop
3. n: 
4. f: nAlph
5. g: Alphn
6. g o f = Id
7. f o g = Id
8. EquivRel x,y:Alph*. x E y
9. 
x,y:Alph*. Dec(x E y)
10. h: n*n*
11. x,y:n*. (map(f;x) E map(f;y)) 
h(x) = h(y)
12. x: Alph*
13. map(f o g;x) E map(f;h(map(g;x)))
x E map(f;h(map(g;x)))
By:
RWH (HypC 7) 13
THEN
RWH
(LemmaC
Thm* as:A*. map(Id;as) = as)
13
Generated subgoals:None
About:
