(* Properties with generic slicing ******************************************)
lemma cnx_lref_atom (G) (L):
- â\88\80i. â\87©[i] L â\89\98 â\8b\86 â\86\92 â\9dªG,Lâ\9d« ⊢ ⬈𝐍 #i.
+ â\88\80i. â\87©[i] L â\89\98 â\8b\86 â\86\92 â\9d¨G,Lâ\9d© ⊢ ⬈𝐍 #i.
#G #L #i #Hi #X #H elim (cpx_inv_lref1_drops … H) -H // *
#I #K #V1 #V2 #HLK lapply (drops_mono … Hi … HLK) -L #H destruct
qed.
lemma cnx_lref_unit (G) (L):
- â\88\80I,K,i. â\87©[i] L â\89\98 K.â\93¤[I] â\86\92 â\9dªG,Lâ\9d« ⊢ ⬈𝐍 #i.
+ â\88\80I,K,i. â\87©[i] L â\89\98 K.â\93¤[I] â\86\92 â\9d¨G,Lâ\9d© ⊢ ⬈𝐍 #i.
#G #L #I #K #i #HLK #X #H elim (cpx_inv_lref1_drops … H) -H // *
#Z #Y #V1 #V2 #HLY lapply (drops_mono … HLK … HLY) -L #H destruct
qed.
(* Basic_2A1: was: cnx_inv_delta *)
lemma cnx_inv_lref_pair (G) (L):
- â\88\80I,K,V,i. â\87©[i] L â\89\98 K.â\93\91[I]V â\86\92 â\9dªG,Lâ\9d« ⊢ ⬈𝐍 #i → ⊥.
+ â\88\80I,K,V,i. â\87©[i] L â\89\98 K.â\93\91[I]V â\86\92 â\9d¨G,Lâ\9d© ⊢ ⬈𝐍 #i → ⊥.
#G #L #I #K #V #i #HLK #H
elim (lifts_total V (𝐔❨↑i❩)) #W #HVW
lapply (H W ?) -H /2 width=7 by cpx_delta_drops/ -HLK