(* Basic_1: was: lift1_lref *)
lemma lifts_inv_lref1: ∀T2,des,i1. ⇧*[des] #i1 ≡ T2 →
- ∃∃i2. @[i1] des ≡ i2 & T2 = #i2.
+ ∃∃i2. @⦃i1, des⦄ ≡ i2 & T2 = #i2.
#T2 #des elim des -des
[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3/
| #d #e #des #IH #i1 #H
qed-.
(* Basic_1: was: lift1_bind *)
-lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] ⓑ{I} V1. U1 ≡ T2 →
+lemma lifts_inv_bind1: ∀a,I,T2,des,V1,U1. ⇧*[des] ⓑ{a,I} V1. U1 ≡ T2 →
∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des + 1] U1 ≡ U2 &
- T2 = ⓑ{I} V2. U2.
-#I #T2 #des elim des -des
+ T2 = ⓑ{a,I} V2. U2.
+#a #I #T2 #des elim des -des
[ #V1 #U1 #H
<(lifts_inv_nil … H) -H /2 width=5/
| #d #e #des #IHdes #V1 #U1 #H
(* Basic forward lemmas *****************************************************)
-lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T1] → 𝐒[T2].
+lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
qed-.
-lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T2] → 𝐒[T1].
+lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
qed-.
(* Basic properties *********************************************************)
-lemma lifts_bind: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
+lemma lifts_bind: ∀a,I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
∀T1. ⇧*[des + 1] T1 ≡ T2 →
- ⇧*[des] ⓑ{I} V1. T1 ≡ ⓑ{I} V2. T2.
-#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
+ ⇧*[des] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2.
+#a #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
[ #V #T1 #H >(lifts_inv_nil … H) -H //
| #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
elim (lifts_inv_cons … H) -H /3 width=3/