-lemma lfpr_fsge_comp: ∀h,G. lfxs_fsge_compatible (λL. cpm h G L 0).
-/4 width=5 by cpm_fwd_cpx, lfpx_fsge_comp, lfxs_co/ qed-.
+lemma rpr_fsge_comp (h) (G):
+ rex_fsge_compatible (λL. cpm h G L 0).
+/4 width=5 by cpm_fwd_cpx, rpx_fsge_comp, rex_co/ qed-.