(**************************************************************************)
include "basic_2/static/lsuba.ma".
-include "basic_2/computation/gcp_aaa.ma".
+include "basic_2/rt_computation/gcp_aaa.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
-(* properties concerning lenv refinement for atomic arity assignment ********)
+(* Properties with lenv refinement for atomic arity assignment **************)
lemma lsuba_lsubc: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → G ⊢ L1 ⫃[RP] L2.