(* Auxiliary inversion lemmas ***********************************************)
-fact lsubr_inv_bind1_aux: â\88\80L1,L2. L1 â\8a\91 L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
+fact lsubr_inv_bind1_aux: â\88\80L1,L2. L1 â«\83 L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
∨∨ L2 = ⋆
- | â\88\83â\88\83K2. K1 â\8a\91 K2 & L2 = K2.ⓑ{I}X
- | â\88\83â\88\83K2,V,W. K1 â\8a\91 K2 & L2 = K2.ⓛW &
+ | â\88\83â\88\83K2. K1 â«\83 K2 & L2 = K2.ⓑ{I}X
+ | â\88\83â\88\83K2,V,W. K1 â«\83 K2 & L2 = K2.ⓛW &
I = Abbr & X = ⓝW.V.
#L1 #L2 * -L1 -L2
[ #L #J #K1 #X #H destruct /2 width=1 by or3_intro0/
]
qed-.
-lemma lsubr_inv_bind1: â\88\80I,K1,L2,X. K1.â\93\91{I}X â\8a\91 L2 →
+lemma lsubr_inv_bind1: â\88\80I,K1,L2,X. K1.â\93\91{I}X â«\83 L2 →
∨∨ L2 = ⋆
- | â\88\83â\88\83K2. K1 â\8a\91 K2 & L2 = K2.ⓑ{I}X
- | â\88\83â\88\83K2,V,W. K1 â\8a\91 K2 & L2 = K2.ⓛW &
+ | â\88\83â\88\83K2. K1 â«\83 K2 & L2 = K2.ⓑ{I}X
+ | â\88\83â\88\83K2,V,W. K1 â«\83 K2 & L2 = K2.ⓛW &
I = Abbr & X = ⓝW.V.
/2 width=3 by lsubr_inv_bind1_aux/ qed-.