(* Properties with syntactic equivalence on referred entries ****************)
-lemma req_reqx_trans: ∀L1,L,T1. L1 ≡[T1] L →
+lemma req_feqx_trans: ∀L1,L,T1. L1 ≡[T1] L →
∀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