(* Note: the constant 0 cannot be generalized *)
lemma lsubsv_drop_O1_conf: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
- â\88\80K1,b,k. â¬\87[b, 0, k] L1 â\89¡ K1 →
- â\88\83â\88\83K2. G â\8a¢ K1 â«\83¡[h, o] K2 & â¬\87[b, 0, k] L2 â\89¡ K2.
+ â\88\80K1,b,k. â¬\87[b, 0, k] L1 â\89\98 K1 →
+ â\88\83â\88\83K2. G â\8a¢ K1 â«\83¡[h, o] K2 & â¬\87[b, 0, k] L2 â\89\98 K2.
#h #o #G #L1 #L2 #H elim H -L1 -L2
[ /2 width=3 by ex2_intro/
| #I #L1 #L2 #V #_ #IHL12 #K1 #b #k #H
(* Note: the constant 0 cannot be generalized *)
lemma lsubsv_drop_O1_trans: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
- â\88\80K2,b, k. â¬\87[b, 0, k] L2 â\89¡ K2 →
- â\88\83â\88\83K1. G â\8a¢ K1 â«\83¡[h, o] K2 & â¬\87[b, 0, k] L1 â\89¡ K1.
+ â\88\80K2,b, k. â¬\87[b, 0, k] L2 â\89\98 K2 →
+ â\88\83â\88\83K1. G â\8a¢ K1 â«\83¡[h, o] K2 & â¬\87[b, 0, k] L1 â\89\98 K1.
#h #o #G #L1 #L2 #H elim H -L1 -L2
[ /2 width=3 by ex2_intro/
| #I #L1 #L2 #V #_ #IHL12 #K2 #b #k #H