(* properties concerning lenv refinement for atomic arity assignment ********)
lemma lsubc_lsuba: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
(* properties concerning lenv refinement for atomic arity assignment ********)
lemma lsubc_lsuba: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →