(* Properties on degree assignment ******************************************)
lemma lsubd_da_trans: ∀h,g,G,L2,T,l. ⦃G, L2⦄ ⊢ T ▪[h, g] l →
(* Properties on degree assignment ******************************************)
lemma lsubd_da_trans: ∀h,g,G,L2,T,l. ⦃G, L2⦄ ⊢ T ▪[h, g] l →
- â\88\80L1. G â\8a¢ L1 â\96ªâ\8a\91[h, g] L2 → ⦃G, L1⦄ ⊢ T ▪[h, g] l.
+ â\88\80L1. G â\8a¢ L1 â«\83â\96ª[h, g] L2 → ⦃G, L1⦄ ⊢ T ▪[h, g] l.
elim (lsubd_inv_pair2 … H) -H * #K1 [ | -IHV -HLK1 ]
[ #HK12 #H destruct /3 width=4/
| #W #l0 #_ #_ #_ #H destruct
]
| #G #L2 #K2 #W #i #l #HLK2 #HW #IHW #L1 #HL12
elim (lsubd_inv_pair2 … H) -H * #K1 [ | -IHV -HLK1 ]
[ #HK12 #H destruct /3 width=4/
| #W #l0 #_ #_ #_ #H destruct
]
| #G #L2 #K2 #W #i #l #HLK2 #HW #IHW #L1 #HL12
elim (lsubd_inv_pair2 … H) -H * #K1 [ -HW | -IHW ]
[ #HK12 #H destruct /3 width=4/
| #V #l0 #HV #H0W #_ #_ #H destruct
elim (lsubd_inv_pair2 … H) -H * #K1 [ -HW | -IHW ]
[ #HK12 #H destruct /3 width=4/
| #V #l0 #HV #H0W #_ #_ #H destruct
qed-.
lemma lsubd_da_conf: ∀h,g,G,L1,T,l. ⦃G, L1⦄ ⊢ T ▪[h, g] l →
qed-.
lemma lsubd_da_conf: ∀h,g,G,L1,T,l. ⦃G, L1⦄ ⊢ T ▪[h, g] l →
- â\88\80L2. G â\8a¢ L1 â\96ªâ\8a\91[h, g] L2 → ⦃G, L2⦄ ⊢ T ▪[h, g] l.
+ â\88\80L2. G â\8a¢ L1 â«\83â\96ª[h, g] L2 → ⦃G, L2⦄ ⊢ T ▪[h, g] l.
elim (lsubd_inv_pair1 … H) -H * #K2 [ -HV | -IHV ]
[ #HK12 #H destruct /3 width=4/
| #W0 #V0 #l0 #HV0 #HW0 #_ #_ #H1 #H2 destruct
elim (lsubd_inv_pair1 … H) -H * #K2 [ -HV | -IHV ]
[ #HK12 #H destruct /3 width=4/
| #W0 #V0 #l0 #HV0 #HW0 #_ #_ #H1 #H2 destruct
lapply (da_mono … H0V0 … HV0) -H0V0 -HV0 #H destruct /2 width=4/
]
| #G #L1 #K1 #W #i #l #HLK1 #HW #IHW #L2 #HL12
lapply (da_mono … H0V0 … HV0) -H0V0 -HV0 #H destruct /2 width=4/
]
| #G #L1 #K1 #W #i #l #HLK1 #HW #IHW #L2 #HL12
elim (lsubd_inv_pair1 … H) -H * #K2 [ -HW | -IHW ]
[ #HK12 #H destruct /3 width=4/
| #W0 #V0 #l0 #HV0 #HW0 #_ #H destruct
elim (lsubd_inv_pair1 … H) -H * #K2 [ -HW | -IHW ]
[ #HK12 #H destruct /3 width=4/
| #W0 #V0 #l0 #HV0 #HW0 #_ #H destruct