1 definition dropable_dx: predicate (relation lenv) ≝
2 λR. ∀L1,L2. R L1 L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 →
3 ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & R K1 K2.
5 lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R).
6 #R #HR #L1 #L2 #H elim H -L2
7 [ #L2 #HL12 #K2 #c #k #HLK2 elim (HR … HL12 … HLK2) -HR -L2
8 /3 width=3 by inj, ex2_intro/
9 | #L #L2 #_ #HL2 #IHL1 #K2 #c #k #HLK2 elim (HR … HL2 … HLK2) -HR -L2
10 #K #HLK #HK2 elim (IHL1 … HLK) -L
11 /3 width=5 by step, ex2_intro/
16 fact lpx_sn_dropable_aux: ∀R,L2,K2,c,l,k. ⬇[c, l, k] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
17 l = 0 → ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & lpx_sn R K1 K2.
18 #R #L2 #K2 #c #l #k #H elim H -L2 -K2 -l -k
19 [ #l #k #Hm #X #H >(lpx_sn_inv_atom2 … H) -H
20 /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/
21 | #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H
22 #K1 #V1 #HK12 #HV12 #H destruct
23 /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/
24 | #I #L2 #K2 #V2 #k #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H
25 #L1 #V1 #HL12 #HV12 #H destruct
26 elim (IHLK2 … HL12) -L2 /3 width=3 by drop_drop, ex2_intro/
27 | #I #L2 #K2 #V2 #W2 #l #k #_ #_ #_ #L1 #_ #H elim (ysucc_inv_O_dx … H)
31 lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R).
32 /2 width=5 by lpx_sn_dropable_aux/ qed-.
34 lemma lpx_sn_drop_trans: ∀R,L1,L2. lpx_sn R L1 L2 →
35 ∀I,K2,V2,i. ⬇[i] L2 ≡ K2.ⓑ{I}V2 →
36 ∃∃K1,V1. ⬇[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2.
37 #R #L1 #L2 #H elim H -L1 -L2
38 [ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct
39 | #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H
40 [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/
41 | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10
42 /3 width=5 by drop_drop_lt, ex3_2_intro/
47 lemma lpx_sn_drop_conf: ∀R,L1,L2. lpx_sn R L1 L2 →
48 ∀I,K1,V1,i. ⬇[i] L1 ≡ K1.ⓑ{I}V1 →
49 ∃∃K2,V2. ⬇[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2.
50 #R #L1 #L2 #H elim H -L1 -L2
51 [ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct
52 | #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H
53 [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/
54 | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10
55 /3 width=5 by drop_drop_lt, ex3_2_intro/