-(* Basic_1: was pr3_gen_appl *)
-lemma cprs_inv_appl1: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 →
- ∨∨ ∃∃V2,T2. L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 &
- U2 = ⓐV2. T2
- | ∃∃a,V2,W,T. L ⊢ V1 ➡* V2 &
- L ⊢ T1 ➡* ⓛ{a}W. T & L ⊢ ⓓ{a}V2. T ➡* U2
- | ∃∃a,V0,V2,V,T. L ⊢ V1 ➡* V0 & ⇧[0,1] V0 ≡ V2 &
- L ⊢ T1 ➡* ⓓ{a}V. T & L ⊢ ⓓ{a}V. ⓐV2. T ➡* U2.
-#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 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct
- lapply (cprs_strap1 … HV10 … HV02) -V0 /5 width=7/
- | #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-.
-