- (∀G1,L1,T1. ❪G0,L0,T0❫ >[h] ❪G1,L1,T1❫ → IH_cnv_cpm_trans_lpr h a G1 L1 T1) →
- ∀G1,L1,T1. ❪G0,L0,T0❫ >[h] ❪G1,L1,T1❫ → IH_cnv_cpms_trans_lpr h a G1 L1 T1.
+ (∀G1,L1,T1. ❪G0,L0,T0❫ > ❪G1,L1,T1❫ → IH_cnv_cpm_trans_lpr h a G1 L1 T1) →
+ ∀G1,L1,T1. ❪G0,L0,T0❫ > ❪G1,L1,T1❫ → IH_cnv_cpms_trans_lpr h a G1 L1 T1.