-| lifts_cons: ∀T1,T,T2,des,d,e.
- ⬆[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2
+| lifts_cons: ∀T1,T,T2,des,l,m.
+ ⬆[l,m] T1 ≡ T → lifts des T T2 → lifts ({l, m} @ des) T1 T2
fact lifts_inv_nil_aux: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 → des = ◊ → T1 = T2.
#T1 #T2 #des * -T1 -T2 -des //
fact lifts_inv_nil_aux: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 → des = ◊ → T1 = T2.
#T1 #T2 #des * -T1 -T2 -des //
qed-.
lemma lifts_inv_nil: ∀T1,T2. ⬆*[◊] T1 ≡ T2 → T1 = T2.
/2 width=3 by lifts_inv_nil_aux/ qed-.
fact lifts_inv_cons_aux: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 →
qed-.
lemma lifts_inv_nil: ∀T1,T2. ⬆*[◊] T1 ≡ T2 → T1 = T2.
/2 width=3 by lifts_inv_nil_aux/ qed-.
fact lifts_inv_cons_aux: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 →
- ∀d,e,tl. des = {d, e} @ tl →
- ∃∃T. ⬆[d, e] T1 ≡ T & ⬆*[tl] T ≡ T2.
+ ∀l,m,tl. des = {l, m} @ tl →
+ ∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[tl] T ≡ T2.
-lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⬆*[{d, e} @ des] T1 ≡ T2 →
- ∃∃T. ⬆[d, e] T1 ≡ T & ⬆*[des] T ≡ T2.
+lemma lifts_inv_cons: ∀T1,T2,l,m,des. ⬆*[{l, m} @ des] T1 ≡ T2 →
+ ∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[des] T ≡ T2.
/2 width=3 by lifts_inv_cons_aux/ qed-.
(* Basic_1: was: lift1_sort *)
lemma lifts_inv_sort1: ∀T2,k,des. ⬆*[des] ⋆k ≡ T2 → T2 = ⋆k.
#T2 #k #des elim des -des
[ #H <(lifts_inv_nil … H) -H //
/2 width=3 by lifts_inv_cons_aux/ qed-.
(* Basic_1: was: lift1_sort *)
lemma lifts_inv_sort1: ∀T2,k,des. ⬆*[des] ⋆k ≡ T2 → T2 = ⋆k.
#T2 #k #des elim des -des
[ #H <(lifts_inv_nil … H) -H //
∃∃i2. @⦃i1, des⦄ ≡ i2 & T2 = #i2.
#T2 #des elim des -des
[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3 by at_nil, ex2_intro/
∃∃i2. @⦃i1, des⦄ ≡ i2 & T2 = #i2.
#T2 #des elim des -des
[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3 by at_nil, ex2_intro/
lemma lifts_inv_gref1: ∀T2,p,des. ⬆*[des] §p ≡ T2 → T2 = §p.
#T2 #p #des elim des -des
[ #H <(lifts_inv_nil … H) -H //
lemma lifts_inv_gref1: ∀T2,p,des. ⬆*[des] §p ≡ T2 → T2 = §p.
#T2 #p #des elim des -des
[ #H <(lifts_inv_nil … H) -H //
#a #I #T2 #des elim des -des
[ #V1 #U1 #H
<(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/
#a #I #T2 #des elim des -des
[ #V1 #U1 #H
<(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/
#I #T2 #des elim des -des
[ #V1 #U1 #H
<(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/
#I #T2 #des elim des -des
[ #V1 #U1 #H
<(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/
⬆*[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 //
⬆*[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 //
⬆*[des] ⓕ{I} V1. T1 ≡ ⓕ{I} V2. T2.
#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
[ #V #T1 #H >(lifts_inv_nil … H) -H //
⬆*[des] ⓕ{I} V1. T1 ≡ ⓕ{I} V2. T2.
#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
[ #V #T1 #H >(lifts_inv_nil … H) -H //
elim (lifts_inv_cons … H) -H /3 width=3 by lift_flat, lifts_cons/
]
qed.
lemma lifts_total: ∀des,T1. ∃T2. ⬆*[des] T1 ≡ T2.
#des elim des -des /2 width=2 by lifts_nil, ex_intro/
elim (lifts_inv_cons … H) -H /3 width=3 by lift_flat, lifts_cons/
]
qed.
lemma lifts_total: ∀des,T1. ∃T2. ⬆*[des] T1 ≡ T2.
#des elim des -des /2 width=2 by lifts_nil, ex_intro/