- [ #X #H #H0
- elim (cprs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H
- [ -H1T elim (H0 ?) -H0 //
- | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/
- ]
- | -L -K -V -V1 -V2 elim Vs -Vs //
+ #X #H #H0
+ elim (cprs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H
+ [ -H1T elim (H0 ?) -H0 //
+ | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/