-lemma jsx_inv_push_sn (h) (G):
- ∀f,I,K1,L2. G ⊢ K1.ⓘ{I} ⊒[h,⫯f] L2 →
- ∃∃K2. G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓘ{I}.
-/2 width=5 by jsx_inv_push_sn_aux/ qed-.
-
-fact jsx_inv_unit_sn_aux (h) (G):
- ∀g,L1,L2. G ⊢ L1 ⊒[h,g] L2 →
- ∀f,I,K1. g = ↑f → L1 = K1.ⓤ{I} →
- ∃∃K2. G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓧ.
-#h #G #g #L1 #L2 * -g -L1 -L2
-[ #f #g #J #L1 #_ #H destruct
-| #f #I #K1 #K2 #_ #g #J #L1 #H
- elim (discr_push_next … H)
-| #f #I #K1 #K2 #HK12 #g #J #L1 #H1 #H2 destruct
- <(injective_next … H1) -g /2 width=3 by ex2_intro/
-| #f #I #K1 #K2 #V #_ #_ #g #J #L1 #_ #H destruct
-]
-qed-.
-
-lemma jsx_inv_unit_sn (h) (G):
- ∀f,I,K1,L2. G ⊢ K1.ⓤ{I} ⊒[h,↑f] L2 →
- ∃∃K2. G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓧ.
-/2 width=6 by jsx_inv_unit_sn_aux/ qed-.
-
-fact jsx_inv_pair_sn_aux (h) (G):
- ∀g,L1,L2. G ⊢ L1 ⊒[h,g] L2 →
- ∀f,I,K1,V. g = ↑f → L1 = K1.ⓑ{I}V →
- ∃∃K2. G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓧ.
-#h #G #g #L1 #L2 * -g -L1 -L2
-[ #f #g #J #L1 #W #_ #H destruct
-| #f #I #K1 #K2 #_ #g #J #L1 #W #H
- elim (discr_push_next … H)
-| #f #I #K1 #K2 #_ #g #J #L1 #W #_ #H destruct
-| #f #I #K1 #K2 #V #HV #HK12 #g #J #L1 #W #H1 #H2 destruct
- <(injective_next … H1) -g /2 width=4 by ex3_intro/
-]
-qed-.
-
-(* Basic_2A1: uses: lcosx_inv_pair *)
-lemma jsx_inv_pair_sn (h) (G):
- ∀f,I,K1,L2,V. G ⊢ K1.ⓑ{I}V ⊒[h,↑f] L2 →
- ∃∃K2. G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓧ.
-/2 width=6 by jsx_inv_pair_sn_aux/ qed-.