(* Basic_2A1: was: llpx_sn_lrefl *)
(* Basic_2A1: this should have been lleq_fwd_llpx_sn *)
lemma req_fwd_rex: ∀R. c_reflexive … R →
- ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤[R, T] L2.
+ ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤[R,T] L2.
#R #HR #L1 #L2 #T * #f #Hf #HL12
/4 width=7 by sex_co, cext2_co, ex2_intro/
qed-.