lemma cpcs_inv_cprs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 →
∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T.
#G #L #T1 #T2 #H @(cpcs_ind … H) -T2
-[ /3 width=3/
+[ /3 width=3 by ex2_intro/
| #T #T2 #_ #HT2 * #T0 #HT10 elim HT2 -HT2 #HT2 #HT0
[ elim (cprs_strip … HT0 … HT2) -T /3 width=3 by cprs_strap1, ex2_intro/
| /3 width=5 by cprs_strap2, ex2_intro/
qed-.
(* Basic_1: was: pc3_gen_sort *)
-lemma cpcs_inv_sort: ∀G,L,k1,k2. ⦃G, L⦄ ⊢ ⋆k1 ⬌* ⋆k2 → k1 = k2.
-#G #L #k1 #k2 #H elim (cpcs_inv_cprs … H) -H
+lemma cpcs_inv_sort: ∀G,L,s1,s2. ⦃G, L⦄ ⊢ ⋆s1 ⬌* ⋆s2 → s1 = s2.
+#G #L #s1 #s2 #H elim (cpcs_inv_cprs … H) -H
#T #H1 >(cprs_inv_sort1 … H1) -T #H2
lapply (cprs_inv_sort1 … H2) -L #H destruct //
qed-.
/3 width=1 by cpcs_inv_abst1, cpcs_sym/ qed-.
(* Basic_1: was: pc3_gen_sort_abst *)
-lemma cpcs_inv_sort_abst: ∀a,G,L,W,T,k. ⦃G, L⦄ ⊢ ⋆k ⬌* ⓛ{a}W.T → ⊥.
-#a #G #L #W #T #k #H
+lemma cpcs_inv_sort_abst: ∀a,G,L,W,T,s. ⦃G, L⦄ ⊢ ⋆s ⬌* ⓛ{a}W.T → ⊥.
+#a #G #L #W #T #s #H
elim (cpcs_inv_cprs … H) -H #X #H1
>(cprs_inv_sort1 … H1) -X #H2
elim (cprs_inv_abst1 … H2) -H2 #W0 #T0 #_ #_ #H destruct
qed-.
(* Basic_1: was: pc3_gen_lift *)
-lemma cpcs_inv_lift: ∀G,L,K,s,d,e. ⇩[s, d, e] L ≡ K →
- â\88\80T1,U1. â\87§[d, e] T1 â\89¡ U1 â\86\92 â\88\80T2,U2. â\87§[d, e] T2 ≡ U2 →
+lemma cpcs_inv_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≡ K →
+ â\88\80T1,U1. â¬\86[l, k] T1 â\89¡ U1 â\86\92 â\88\80T2,U2. â¬\86[l, k] T2 ≡ U2 →
⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, K⦄ ⊢ T1 ⬌* T2.
-#G #L #K #s #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12
+#G #L #K #b #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12
elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2
elim (cprs_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1
elim (cprs_inv_lift1 … HU2 … HLK … HTU2) -L -U2 #X #HXU
->(lift_inj … HXU … HTU) -X -U -d -e /2 width=3 by cprs_div/
+>(lift_inj … HXU … HTU) -X -U -l -k /2 width=3 by cprs_div/
qed-.
(* Advanced properties ******************************************************)
(* Basic_1: was: pc3_wcpr0_t *)
(* Basic_1: note: pc3_wcpr0_t should be renamed *)
+(* Note: alternative proof /3 width=5 by lprs_cprs_conf, lpr_lprs/ *)
lemma lpr_cprs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 →
∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
-/3 width=5 by lprs_cprs_conf, lpr_lprs/ qed-.
+#G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (cprs_lpr_conf_dx … HT12 … HL12) -L1
+/2 width=3 by cprs_div/
+qed-.
(* Basic_1: was only: pc3_pr0_pr2_t *)
(* Basic_1: note: pc3_pr0_pr2_t should be renamed *)
qed.
lemma lsubr_cpcs_trans: ∀G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 →
- â\88\80L2. L2 â\8a\91 L1 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
+ â\88\80L2. L2 â«\83 L1 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
#G #L1 #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12
/3 width=5 by cprs_div, lsubr_cprs_trans/
qed-.
(* Basic_1: was: pc3_lift *)
-lemma cpcs_lift: ∀G,L,K,s,d,e. ⇩[s, d, e] L ≡ K →
- â\88\80T1,U1. â\87§[d, e] T1 â\89¡ U1 â\86\92 â\88\80T2,U2. â\87§[d, e] T2 ≡ U2 →
+lemma cpcs_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≡ K →
+ â\88\80T1,U1. â¬\86[l, k] T1 â\89¡ U1 â\86\92 â\88\80T2,U2. â¬\86[l, k] T2 ≡ U2 →
⦃G, K⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ U1 ⬌* U2.
-#G #L #K #s #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12
+#G #L #K #b #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12
elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
-elim (lift_total T d e) /3 width=12 by cprs_div, cprs_lift/
+elim (lift_total T l k) /3 width=12 by cprs_div, cprs_lift/
qed.
lemma cpcs_strip: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ⬌* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌ T2 →
(* More inversion lemmas ****************************************************)
+(* Note: there must be a proof suitable for llpr *)
lemma cpcs_inv_abst_sn: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 →
∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬌* T2 & a1 = a2.
#a1 #a2 #G #L #W1 #W2 #T1 #T2 #H