+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_1: was pr3_gen_appl *)
+lemma cprs_inv_appl1: ∀G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡* U2 →
+ ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L⦄ ⊢ T1 ➡* T2 &
+ U2 = ⓐV2. T2
+ | ∃∃a,W,T. ⦃G, L⦄ ⊢ T1 ➡* ⓛ{a}W.T &
+ ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V1.T ➡* U2
+ | ∃∃a,V0,V2,V,T. ⦃G, L⦄ ⊢ V1 ➡* V0 & ⇧[0,1] V0 ≡ V2 &
+ ⦃G, L⦄ ⊢ T1 ➡* ⓓ{a}V.T &
+ ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡* U2.
+#G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 [ /3 width=5/ ]
+#U #U2 #_ #HU2 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+ elim (cpr_inv_appl1 … HU2) -HU2 *
+ [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
+ | #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct
+ lapply (cprs_strap1 … HV10 … HV02) -V0 #HV12
+ lapply (lsubr_cpr_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 /2 width=1/ #HT2
+ @or3_intro1 @(ex2_3_intro … HT10) -HT10 /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
+ | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
+ @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
+ ]
+| /4 width=9/
+| /4 width=11/
+]
+qed-.
+