2. A: T List
3. B: T List
4. no_repeats(T;A)
5.
x:T. (x 
A) 
(x B)
f:(
||A||
||B||). Inj(||A||; ||B||; f)
T:Type, A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) ||A||
||B||
k,m:. (f:(km). Inj(k; m; f)) km
| 1 | 1. T: Type 2. A: T List 3. B: T List 4. no_repeats(T;A) 5. x:T. (x A) (x B) f:(||A||||B||). Inj(||A||; ||B||; f) | 9 steps |
About:
 |  |  |  |  |  |  |