- lapply (lsuby_cpy_trans … HT1 (L.ⓑ{I}V) ?) -HT1 /2 width=1 by lsuby_succ/
- lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /3 width=5 by cpy_bind, lsuby_succ, ex2_intro/
+ lapply (lsuby_cpy_trans … HT1 (L.ⓑ{I}V1) ?) -HT1 /2 width=1 by lsuby_succ/
+ lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V2) ?) -HT2
+ /3 width=5 by cpy_bind, lsuby_succ, ex2_intro/