∀G1,G2,L2,T2. ❪G1,L,T1❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫.
#L1 #L #T1 #HL1 #G1 #G2 #L2 #T2 #H
elim (feqx_inv_gen_sn … H) -H #H #HL2 #T12 destruct
∀G1,G2,L2,T2. ❪G1,L,T1❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫.
#L1 #L #T1 #HL1 #G1 #G2 #L2 #T2 #H
elim (feqx_inv_gen_sn … H) -H #H #HL2 #T12 destruct