At: fin listify 1 1 1 1 1 1 1
1. T: Type
2. n: 
3. f: n
T
4. Inj(n; T; f)
5. 
b:T. 
a:n. f(a) = b
6. t: T
7. a: n
8. f(a) = t
9. ((f)[n])[a] = f(a)
10. mem_f(T;((f)[n])[a];(f)[n])
mem_f(T;t;(f)[n])
By:
RWH (HypC -2) -1
THEN
RWH (HypC -3) -1
Generated subgoals:None
About:
