-lemma cpr_inv_sort1: ∀G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ➡ T2 → T2 = ⋆s.
-#G #L #T2 #s #H
-elim (cpr_inv_atom1 … H) -H //
-* #K #V #V2 #i #_ #_ #_ #H destruct
-qed-.
-
-(* Basic_1: includes: pr0_gen_lref pr2_gen_lref *)
-lemma cpr_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡ T2 →
- T2 = #i ∨
- ∃∃K,V,V2. ⬇[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
- ⬆[O, i + 1] V2 ≡ T2.
-#G #L #T2 #i #H
-elim (cpr_inv_atom1 … H) -H /2 width=1 by or_introl/
-* #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=6 by ex3_3_intro, or_intror/
-qed-.
-
-lemma cpr_inv_gref1: ∀G,L,T2,p. ⦃G, L⦄ ⊢ §p ➡ T2 → T2 = §p.
-#G #L #T2 #p #H
-elim (cpr_inv_atom1 … H) -H //
-* #K #V #V2 #i #_ #_ #_ #H destruct
-qed-.
-
-fact cpr_inv_bind1_aux: ∀G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ➡ U2 →
- ∀a,I,V1,T1. U1 = ⓑ{a,I}V1. T1 → (
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡ T2 &
- U2 = ⓑ{a,I}V2.T2
- ) ∨
- ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡ T & ⬆[0, 1] U2 ≡ T &
- a = true & I = Abbr.
-#G #L #U1 #U2 * -L -U1 -U2
-[ #I #G #L #b #J #W1 #U1 #H destruct
-| #L #G #K #V #V2 #W2 #i #_ #_ #_ #b #J #W #U1 #H destruct
-| #a #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W #U1 #H destruct /3 width=5 by ex3_2_intro, or_introl/
-| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W #U1 #H destruct
-| #G #L #V #T1 #T #T2 #HT1 #HT2 #b #J #W #U1 #H destruct /3 width=3 by ex4_intro, or_intror/
-| #G #L #V #T1 #T2 #_ #b #J #W #U1 #H destruct
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #b #J #W #U1 #H destruct
-| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #b #J #W #U1 #H destruct
-]
-qed-.
-
-lemma cpr_inv_bind1: ∀a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡ U2 → (
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡ T2 &
- U2 = ⓑ{a,I}V2.T2
- ) ∨
- ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡ T & ⬆[0, 1] U2 ≡ T &
- a = true & I = Abbr.
-/2 width=3 by cpr_inv_bind1_aux/ qed-.
-
-(* Basic_1: includes: pr0_gen_abbr pr2_gen_abbr *)
-lemma cpr_inv_abbr1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡ U2 → (
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L. ⓓV1⦄ ⊢ T1 ➡ T2 &
- U2 = ⓓ{a}V2.T2
- ) ∨
- ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡ T & ⬆[0, 1] U2 ≡ T & a = true.
-#a #G #L #V1 #T1 #U2 #H
-elim (cpr_inv_bind1 … H) -H *
-/3 width=5 by ex3_2_intro, ex3_intro, or_introl, or_intror/