(* Advanced properties ******************************************************)
lemma fqup_zeta (b) (p) (I) (G) (K) (V):
- â\88\80T1,T2. â¬\86*[1]T2 ≘ T1 → ⦃G,K,ⓑ{p,I}V.T1⦄ ⬂+[b] ⦃G,K,T2⦄.
+ â\88\80T1,T2. â\87§*[1]T2 ≘ T1 → ⦃G,K,ⓑ{p,I}V.T1⦄ ⬂+[b] ⦃G,K,T2⦄.
* /4 width=5 by fqup_strap2, fqu_fqup, fqu_drop, fqu_clear, fqu_bind_dx/ qed.
(* Basic_2A1: removed theorems 1: fqup_drop *)