-definition d_liftable1: relation2 lenv term → predicate bool ≝
- λR,b. ∀f,L,K. ⬇*[b, f] L ≡ K →
- ∀T,U. ⬆*[f] T ≡ U → R K T → R L U.
-
-definition d_liftable2: predicate (lenv → relation term) ≝
- λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K →
- ∀U1. ⬆*[f] T1 ≡ U1 →
- ∃∃U2. ⬆*[f] T2 ≡ U2 & R L U1 U2.
-
-definition d_deliftable2_sn: predicate (lenv → relation term) ≝
- λR. ∀L,U1,U2. R L U1 U2 → ∀b,f,K. ⬇*[b, f] L ≡ K →
- ∀T1. ⬆*[f] T1 ≡ U1 →
- ∃∃T2. ⬆*[f] T2 ≡ U2 & R K T1 T2.
-
-definition dropable_sn: predicate (rtmap → relation lenv) ≝
- λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → ∀f2,L2. R f2 L1 L2 →
- ∀f1. f ~⊚ f1 ≡ f2 →
- ∃∃K2. R f1 K1 K2 & ⬇*[b, f] L2 ≡ K2.
-
-definition 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 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.
+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.