-interpretation "general slicing (local environment)"
- 'RDropStar s t L1 L2 = (drops s t L1 L2).
-
-definition d_liftable1: relation2 lenv term → predicate bool ≝
- λR,s. ∀L,K,t. ⬇*[s, t] L ≡ K →
- ∀T,U. ⬆*[t] T ≡ U → R K T → R L U.
-
-definition d_liftable2: predicate (lenv → relation term) ≝
- λR. ∀K,T1,T2. R K T1 T2 → ∀L,s,t. ⬇*[s, t] L ≡ K →
- ∀U1. ⬆*[t] T1 ≡ U1 →
- ∃∃U2. ⬆*[t] T2 ≡ U2 & R L U1 U2.
-
-definition d_deliftable2_sn: predicate (lenv → relation term) ≝
- λR. ∀L,U1,U2. R L U1 U2 → ∀K,s,t. ⬇*[s, t] L ≡ K →
- ∀T1. ⬆*[t] T1 ≡ U1 →
- ∃∃T2. ⬆*[t] T2 ≡ U2 & R K T1 T2.
-
-definition dropable_sn: predicate (relation lenv) ≝
- λR. ∀L1,K1,s,t. ⬇*[s, t] L1 ≡ K1 → ∀L2. R L1 L2 →
- ∃∃K2. R K1 K2 & ⬇*[s, t] L2 ≡ K2.
-(*
-definition dropable_dx: predicate (relation lenv) ≝
- λR. ∀L1,L2. R L1 L2 → ∀K2,s,m. ⬇[s, 0, m] L2 ≡ K2 →
- ∃∃K1. ⬇[s, 0, m] L1 ≡ K1 & R K1 K2.
-*)
+interpretation "uniform slicing (local environment)"
+ 'RDropStar i L1 L2 = (drops true (uni i) L1 L2).
+
+interpretation "generic slicing (local environment)"
+ 'RDropStar b f L1 L2 = (drops b f L1 L2).
+
+definition d_liftable1: predicate (relation2 lenv term) ≝
+ λR. ∀K,T. R K T → ∀b,f,L. ⬇*[b, f] L ≘ K →
+ ∀U. ⬆*[f] T ≘ U → R L U.
+
+definition d_liftable1_isuni: predicate (relation2 lenv term) ≝
+ λR. ∀K,T. R K T → ∀b,f,L. ⬇*[b, f] L ≘ K → 𝐔⦃f⦄ →
+ ∀U. ⬆*[f] T ≘ U → R L U.
+
+definition d_deliftable1: predicate (relation2 lenv term) ≝
+ λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≘ K →
+ ∀T. ⬆*[f] T ≘ U → R K T.
+
+definition d_deliftable1_isuni: predicate (relation2 lenv term) ≝
+ λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≘ K → 𝐔⦃f⦄ →
+ ∀T. ⬆*[f] T ≘ U → R K T.
+
+definition d_liftable2_sn: ∀C:Type[0]. ∀S:rtmap → relation C.
+ predicate (lenv → relation C) ≝
+ λC,S,R. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≘ K →
+ ∀U1. S f T1 U1 →
+ ∃∃U2. S f T2 U2 & R L U1 U2.
+
+definition d_deliftable2_sn: ∀C:Type[0]. ∀S:rtmap → relation C.
+ predicate (lenv → relation C) ≝
+ λC,S,R. ∀L,U1,U2. R L U1 U2 → ∀b,f,K. ⬇*[b, f] L ≘ K →
+ ∀T1. S f T1 U1 →
+ ∃∃T2. S f T2 U2 & R K T1 T2.
+
+definition d_liftable2_bi: ∀C:Type[0]. ∀S:rtmap → relation C.
+ predicate (lenv → relation C) ≝
+ λC,S,R. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≘ K →
+ ∀U1. S f T1 U1 →
+ ∀U2. S f T2 U2 → R L U1 U2.
+
+definition d_deliftable2_bi: ∀C:Type[0]. ∀S:rtmap → relation C.
+ predicate (lenv → relation C) ≝
+ λC,S,R. ∀L,U1,U2. R L U1 U2 → ∀b,f,K. ⬇*[b, f] L ≘ K →
+ ∀T1. S f T1 U1 →
+ ∀T2. S f T2 U2 → R K T1 T2.
+
+definition co_dropable_sn: predicate (rtmap → relation lenv) ≝
+ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≘ K1 → 𝐔⦃f⦄ →
+ ∀f2,L2. R f2 L1 L2 → ∀f1. f ~⊚ f1 ≘ f2 →
+ ∃∃K2. R f1 K1 K2 & ⬇*[b, f] L2 ≘ K2.
+
+definition co_dropable_dx: predicate (rtmap → relation lenv) ≝
+ λR. ∀f2,L1,L2. R f2 L1 L2 →
+ ∀b,f,K2. ⬇*[b, f] L2 ≘ K2 → 𝐔⦃f⦄ →
+ ∀f1. f ~⊚ f1 ≘ f2 →
+ ∃∃K1. ⬇*[b, f] L1 ≘ K1 & R f1 K1 K2.
+
+definition co_dedropable_sn: predicate (rtmap → relation lenv) ≝
+ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≘ K1 → ∀f1,K2. R f1 K1 K2 →
+ ∀f2. f ~⊚ f1 ≘ f2 →
+ ∃∃L2. R f2 L1 L2 & ⬇*[b, f] L2 ≘ K2 & L1 ≡[f] L2.
+
+(* Basic properties *********************************************************)
+
+lemma drops_atom_F: ∀f. ⬇*[Ⓕ, f] ⋆ ≘ ⋆.
+#f @drops_atom #H destruct
+qed.
+
+lemma drops_eq_repl_back: ∀b,L1,L2. eq_repl_back … (λf. ⬇*[b, f] L1 ≘ L2).
+#b #L1 #L2 #f1 #H elim H -f1 -L1 -L2
+[ /4 width=3 by drops_atom, isid_eq_repl_back/
+| #f1 #I #L1 #L2 #_ #IH #f2 #H elim (eq_inv_nx … H) -H
+ /3 width=3 by drops_drop/
+| #f1 #I1 #I2 #L1 #L2 #_ #HI #IH #f2 #H elim (eq_inv_px … H) -H
+ /3 width=3 by drops_skip, liftsb_eq_repl_back/
+]
+qed-.
+
+lemma drops_eq_repl_fwd: ∀b,L1,L2. eq_repl_fwd … (λf. ⬇*[b, f] L1 ≘ L2).
+#b #L1 #L2 @eq_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *)
+qed-.
+
+(* Basic_2A1: includes: drop_FT *)
+lemma drops_TF: ∀f,L1,L2. ⬇*[Ⓣ, f] L1 ≘ L2 → ⬇*[Ⓕ, f] L1 ≘ L2.
+#f #L1 #L2 #H elim H -f -L1 -L2
+/3 width=1 by drops_atom, drops_drop, drops_skip/
+qed.
+
+(* Basic_2A1: includes: drop_gen *)
+lemma drops_gen: ∀b,f,L1,L2. ⬇*[Ⓣ, f] L1 ≘ L2 → ⬇*[b, f] L1 ≘ L2.
+* /2 width=1 by drops_TF/
+qed-.
+
+(* Basic_2A1: includes: drop_T *)
+lemma drops_F: ∀b,f,L1,L2. ⬇*[b, f] L1 ≘ L2 → ⬇*[Ⓕ, f] L1 ≘ L2.
+* /2 width=1 by drops_TF/
+qed-.
+
+lemma d_liftable2_sn_bi: ∀C,S. (∀f,c. is_mono … (S f c)) →
+ ∀R. d_liftable2_sn C S R → d_liftable2_bi C S R.
+#C #S #HS #R #HR #K #T1 #T2 #HT12 #b #f #L #HLK #U1 #HTU1 #U2 #HTU2
+elim (HR … HT12 … HLK … HTU1) -HR -K -T1 #X #HTX #HUX
+<(HS … HTX … HTU2) -T2 -U2 -b -f //
+qed-.
+
+lemma d_deliftable2_sn_bi: ∀C,S. (∀f. is_inj2 … (S f)) →
+ ∀R. d_deliftable2_sn C S R → d_deliftable2_bi C S R.
+#C #S #HS #R #HR #L #U1 #U2 #HU12 #b #f #K #HLK #T1 #HTU1 #T2 #HTU2
+elim (HR … HU12 … HLK … HTU1) -HR -L -U1 #X #HUX #HTX
+<(HS … HUX … HTU2) -U2 -T2 -b -f //
+qed-.
+