(* Properties with generic slicing for local environments *******************)
-lemma fqup_drops_succ: â\88\80b,G,K,T,i,L,U. â¬\87*[â\86\91i] L â\89\98 K â\86\92 â¬\86*[↑i] T ≘ U →
+lemma fqup_drops_succ: â\88\80b,G,K,T,i,L,U. â\87©*[â\86\91i] L â\89\98 K â\86\92 â\87§*[↑i] T ≘ U →
⦃G,L,U⦄ ⬂+[b] ⦃G,K,T⦄.
#b #G #K #T #i elim i -i
[ #L #U #HLK #HTU elim (drops_inv_succ … HLK) -HLK
]
qed.
-lemma fqup_drops_strap1: â\88\80b,G1,G2,L1,K1,K2,T1,T2,U1,i. â¬\87*[i] L1 â\89\98 K1 â\86\92 â¬\86*[i] T1 ≘ U1 →
+lemma fqup_drops_strap1: â\88\80b,G1,G2,L1,K1,K2,T1,T2,U1,i. â\87©*[i] L1 â\89\98 K1 â\86\92 â\87§*[i] T1 ≘ U1 →
⦃G1,K1,T1⦄ ⬂[b] ⦃G2,K2,T2⦄ → ⦃G1,L1,U1⦄ ⬂+[b] ⦃G2,K2,T2⦄.
#b #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 *
[ #HLK1 #HTU1 #HT12
]
qed-.
-lemma fqup_lref: â\88\80b,I,G,L,K,V,i. â¬\87*[i] L ≘ K.ⓑ{I}V → ⦃G,L,#i⦄ ⬂+[b] ⦃G,K,V⦄.
+lemma fqup_lref: â\88\80b,I,G,L,K,V,i. â\87©*[i] L ≘ K.ⓑ{I}V → ⦃G,L,#i⦄ ⬂+[b] ⦃G,K,V⦄.
/2 width=6 by fqup_drops_strap1/ qed.