(* Basic_2A1: was: llpx_sn_lrefl *)
(* Basic_2A1: this should have been lleq_fwd_llpx_sn *)
lemma req_fwd_rex: ∀R. c_reflexive … R →
(* Basic_2A1: was: llpx_sn_lrefl *)
(* Basic_2A1: this should have been lleq_fwd_llpx_sn *)
lemma req_fwd_rex: ∀R. c_reflexive … R →