-
-lemma llpx_sn_fwd_bind_sn: ∀R,a,I,L1,L2,V,T,l. llpx_sn R l (ⓑ{a,I}V.T) L1 L2 →
- llpx_sn R l V L1 L2.
-#R #a #I #L1 #L2 #V #T #l #H elim (llpx_sn_inv_bind … H) -H //
-qed-.
-
-lemma llpx_sn_fwd_bind_dx: ∀R,a,I,L1,L2,V,T,l. llpx_sn R l (ⓑ{a,I}V.T) L1 L2 →
- llpx_sn R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
-#R #a #I #L1 #L2 #V #T #l #H elim (llpx_sn_inv_bind … H) -H //
-qed-.
-
-lemma llpx_sn_fwd_flat_sn: ∀R,I,L1,L2,V,T,l. llpx_sn R l (ⓕ{I}V.T) L1 L2 →
- llpx_sn R l V L1 L2.
-#R #I #L1 #L2 #V #T #l #H elim (llpx_sn_inv_flat … H) -H //
-qed-.
-
-lemma llpx_sn_fwd_flat_dx: ∀R,I,L1,L2,V,T,l. llpx_sn R l (ⓕ{I}V.T) L1 L2 →
- llpx_sn R l T L1 L2.
-#R #I #L1 #L2 #V #T #l #H elim (llpx_sn_inv_flat … H) -H //
-qed-.
-
-lemma llpx_sn_fwd_pair_sn: ∀R,I,L1,L2,V,T,l. llpx_sn R l (②{I}V.T) L1 L2 →
- llpx_sn R l V L1 L2.
-#R * /2 width=4 by llpx_sn_fwd_flat_sn, llpx_sn_fwd_bind_sn/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma llpx_sn_refl: ∀R. (∀L. reflexive … (R L)) → ∀T,L,l. llpx_sn R l T L L.
-#R #HR #T #L @(f2_ind … rfw … L T) -L -T
-#x #IH #L * * /3 width=1 by llpx_sn_sort, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/
-#i #Hx elim (lt_or_ge i (|L|)) /2 width=1 by llpx_sn_free/
-#HiL #l elim (ylt_split i l) /2 width=1 by llpx_sn_skip/
-elim (drop_O1_lt … HiL) -HiL destruct /4 width=9 by llpx_sn_lref, drop_fwd_rfw/
-qed-.
-
-lemma llpx_sn_Y: ∀R,T,L1,L2. |L1| = |L2| → llpx_sn R (∞) T L1 L2.
-#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
-#x #IH #L1 * * /3 width=1 by llpx_sn_sort, llpx_sn_skip, llpx_sn_gref, llpx_sn_flat/
-#a #I #V1 #T1 #Hx #L2 #HL12
-@llpx_sn_bind /2 width=1 by/ (**) (* explicit constructor *)
-@IH -IH // normalize /2 width=1 by eq_f2/
-qed-.
-
-lemma llpx_sn_ge_up: ∀R,L1,L2,U,lt. llpx_sn R lt U L1 L2 → ∀T,l,k. ⬆[l, k] T ≡ U →
- lt ≤ l + k → llpx_sn R l U L1 L2.
-#R #L1 #L2 #U #lt #H elim H -L1 -L2 -U -lt
-[ #L1 #L2 #lt #s #HL12 #X #l #k #H #_ >(lift_inv_sort2 … H) -H /2 width=1 by llpx_sn_sort/
-| #L1 #L2 #lt #i #HL12 #Hilt #X #l #k #H #Hltlm
- elim (lift_inv_lref2 … H) -H * #Hil #H destruct /3 width=1 by llpx_sn_skip, ylt_inj/ -HL12
- elim (ylt_yle_false … Hilt) -Hilt
- @(yle_trans … Hltlm) /2 width=1 by yle_inj/ (**) (* full auto too slow 11s *)
-| #I #L1 #L2 #K1 #K2 #W1 #W2 #lt #i #Hlti #HLK1 #HLK2 #HW1 #HW12 #_ #X #l #k #H #_
- elim (lift_inv_lref2 … H) -H * #Hil #H destruct
- [ lapply (llpx_sn_fwd_length … HW1) -HW1 #HK12
- lapply (drop_fwd_length … HLK1) lapply (drop_fwd_length … HLK2)
- normalize in ⊢ (%→%→?); -I -W1 -W2 -lt /3 width=1 by llpx_sn_skip, ylt_inj/
- | /3 width=9 by llpx_sn_lref, yle_fwd_plus_sn1/
- ]
-| /2 width=1 by llpx_sn_free/
-| #L1 #L2 #lt #p #HL12 #X #l #k #H #_ >(lift_inv_gref2 … H) -H /2 width=1 by llpx_sn_gref/
-| #a #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #k #H #Hltlm destruct
- elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct
- @(llpx_sn_bind) /2 width=4 by/ (**) (* full auto fails *)
- @(IHT … HTU) /2 width=1 by yle_succ/
-| #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #k #H #Hltlm destruct
- elim (lift_inv_flat2 … H) -H #HVW #HTU #H destruct
- /3 width=4 by llpx_sn_flat/
-]
-qed-.
-
-(**) (* the minor premise comes first *)
-lemma llpx_sn_ge: ∀R,L1,L2,T,l1,l2. l1 ≤ l2 →
- llpx_sn R l1 T L1 L2 → llpx_sn R l2 T L1 L2.
-#R #L1 #L2 #T #l1 #l2 * -l1 -l2 (**) (* destructed yle *)
-/3 width=6 by llpx_sn_ge_up, llpx_sn_Y, llpx_sn_fwd_length, yle_inj/
-qed-.
-
-lemma llpx_sn_bind_O: ∀R,a,I,L1,L2,V,T. llpx_sn R 0 V L1 L2 →
- llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
- llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2.
-/3 width=3 by llpx_sn_ge, llpx_sn_bind/ qed-.
-
-lemma llpx_sn_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
- ∀L1,L2,T,l. llpx_sn R1 l T L1 L2 → llpx_sn R2 l T L1 L2.
-#R1 #R2 #HR12 #L1 #L2 #T #l #H elim H -L1 -L2 -T -l
-/3 width=9 by llpx_sn_sort, llpx_sn_skip, llpx_sn_lref, llpx_sn_free, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/
-qed-.