(* *)
(**************************************************************************)
-include "ground_2/lib/star.ma".
+include "ground/lib/star.ma".
include "static_2/notation/relations/suptermplus_6.ma".
include "static_2/notation/relations/suptermplus_7.ma".
include "static_2/s_transition/fqu.ma".
(* Advanced properties ******************************************************)
lemma fqup_zeta (b) (p) (I) (G) (K) (V):
- ∀T1,T2. ⇧*[1]T2 ≘ T1 → ❪G,K,ⓑ[p,I]V.T1❫ ⬂+[b] ❪G,K,T2❫.
+ ∀T1,T2. ⇧[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 *)