-(* Basic_properties *********************************************************)
-
-lemma frees_req_conf: ∀f,L1,T. L1 ⊢ 𝐅+⦃T⦄ ≘ f →
- ∀L2. L1 ≡[T] L2 → L2 ⊢ 𝐅+⦃T⦄ ≘ f.
-#f #L1 #T #H elim H -f -L1 -T
-[ /2 width=3 by frees_sort/
-| #f #i #Hf #L2 #H2
- >(rex_inv_atom_sn … H2) -L2
- /2 width=1 by frees_atom/
-| #f #I #L1 #V1 #_ #IH #Y #H2
- elim (req_inv_zero_pair_sn … H2) -H2 #L2 #HL12 #H destruct
- /3 width=1 by frees_pair/
-| #f #I #L1 #Hf #Y #H2
- elim (rex_inv_zero_unit_sn … H2) -H2 #g #L2 #_ #_ #H destruct
- /2 width=1 by frees_unit/
-| #f #I #L1 #i #_ #IH #Y #H2
- elim (req_inv_lref_bind_sn … H2) -H2 #J #L2 #HL12 #H destruct
- /3 width=1 by frees_lref/
-| /2 width=1 by frees_gref/
-| #f1V #f1T #f1 #p #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #L2 #H2
- elim (req_inv_bind … H2) -H2 /3 width=5 by frees_bind/
-| #f1V #f1T #f1 #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #L2 #H2
- elim (req_inv_flat … H2) -H2 /3 width=5 by frees_flat/
-]
+lemma req_fwd_reqg (S) (T:term):
+ reflexive … S →
+ ∀L1,L2. L1 ≡[T] L2 → L1 ≛[S,T] L2.
+/3 width=1 by req_fwd_rex, teqg_refl/ qed-.
+
+lemma transitive_req_fwd_rex (R):
+ R_transitive_req R → R_transitive_rex ceq R R.
+#R #HR #L1 #L #T1 #HL1 #T #HT #T2 #HT2
+@(HR … HL1) -HR -HL1 >(teq_inv_eq … HT) -T1 // (**)