(* Basic_1: was: csubc_drop1_conf_rev *)
lemma ldrops_lsubc_trans: ∀RR,RS,RP.
acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
(* Basic_1: was: csubc_drop1_conf_rev *)
lemma ldrops_lsubc_trans: ∀RR,RS,RP.
acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →