At: fin alph list quo11111 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)
h:(Alph*Alph*). (x,y:Alph*. (x E y) h(x) = h(y)) & (x:Alph*. x E (h(x))) By: Inst
Thm*q:, E:(q*q*Prop).
(EquivRel x,y:q*. x E y) & (x,y:q*. Dec(x E y))
(h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x))))
[n;x,y. map(f;x) E map(f;y)]
THEN
Reduce 0 Generated subgoals: