-lemma jsx_fwd_drops_pair_sn (h) (b) (G):
- ∀L1,L2. G ⊢ L1 ⊒[h] L2 →
- â\88\80f. ð\9d\90\94â¦\83fâ¦\84 â\86\92 â\88\80I,K1,V. â¬\87*[b,f]L1 â\89\98 K1.â\93\91{I}V →
- ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⬇*[b,f]L2 ≘ K2.ⓑ{I}V
- | ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⬇*[b,f]L2 ≘ K2.ⓧ & G ⊢ ⬈*[h,V] 𝐒⦃K2⦄.
-#h #b #G #L1 #L2 #H elim H -L1 -L2
+lemma jsx_fwd_drops_pair_sn (b) (G):
+ ∀L1,L2. G ⊢ L1 ⊒ L2 →
+ â\88\80f. ð\9d\90\94â\9dªfâ\9d« â\86\92 â\88\80I,K1,V. â\87©*[b,f]L1 â\89\98 K1.â\93\91[I]V →
+ ∨∨ ∃∃K2. G ⊢ K1 ⊒ K2 & ⇩*[b,f]L2 ≘ K2.ⓑ[I]V
+ | ∃∃K2. G ⊢ K1 ⊒ K2 & ⇩*[b,f]L2 ≘ K2.ⓧ & G ⊢ ⬈*𝐒[V] K2.
+#b #G #L1 #L2 #H elim H -L1 -L2