PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: list quo choice pls 1 1 1 2 1 1 1 2 1
1. q:
2. E: q*q*Prop
3. EquivRel x,y:q*. x E y
4. x,y:q*. Dec(x E y)
5. f: q*
6. g: q*
7. g o f = Id
8. f o g = Id
9. h:
10. n,k:. ((g(n)) E (g(k))) h(n) = h(k)
11. x: q*
12. (g(f(x))) E (g(h(f(x))))

x E ((g o h o f)(x))
By: RWH add_composeC 12
Generated subgoal:

112. ((g o f)(x)) E ((g o h)(f(x)))
x E ((g o h o f)(x))

About:
applyfunctionlistnatural_numberpropallequal