PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: list in mem f list 2 2
1. T: Type
2. a: T
3. as: T*
4. as {x:T| mem_f(T;x;as) }*

as {x:T| a = x mem_f(T;x;as) }*
By: Inclusion1 4
Generated subgoal:

14. as = as {x:T| mem_f(T;x;as) }*
5. zzz: {x:T| mem_f(T;x;as) }*
6. x: {x:T| mem_f(T;x;as) }*
7. u: T
8. mem_f(T;u;as)
a = u mem_f(T;u;as)

About:
memberlistsetorequaluniverse