(* Properties with generic slicing for local environments *******************)
lemma fqus_drops: ∀b,G,L,K,T,U,i. ⬇*[i] L ≘ K → ⬆*[i] T ≘ U →
(* Properties with generic slicing for local environments *******************)
lemma fqus_drops: ∀b,G,L,K,T,U,i. ⬇*[i] L ≘ K → ⬆*[i] T ≘ U →