∀t,h,f:Top. (mapcons(f;[h / t]) ~ [f h t / mapcons(f;t)])
{ (UnivCD THENA Auto) }
1. t : Top@i
2. h : Top@i
3. f : Top@i
⊢ mapcons(f;[h / t]) ~ [f h t / mapcons(f;t)]