∀L1,L2,l,p. |L1| = |L2| → R l (§p) L1 L2
) → (
∀a,I,L1,L2,V,T,l.
∀L1,L2,l,p. |L1| = |L2| → R l (§p) L1 L2
) → (
∀a,I,L1,L2,V,T,l.
- L1 â\89¡[V, l]L2 â\86\92 L1.â\93\91{I}V â\89¡[T, ⫯l] L2.ⓑ{I}V →
- R l V L1 L2 â\86\92 R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R l (ⓑ{a,I}V.T) L1 L2
+ L1 â\89¡[V, l]L2 â\86\92 L1.â\93\91{I}V â\89¡[T, â\86\91l] L2.ⓑ{I}V →
+ R l V L1 L2 â\86\92 R (â\86\91l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R l (ⓑ{a,I}V.T) L1 L2
qed-.
lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,l. L1 ≡[ⓑ{a,I}V.T, l] L2 →
qed-.
lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,l. L1 ≡[ⓑ{a,I}V.T, l] L2 →
/2 width=2 by llpx_sn_inv_bind/ qed-.
lemma lleq_inv_flat: ∀I,L1,L2,V,T,l. L1 ≡[ⓕ{I}V.T, l] L2 →
/2 width=2 by llpx_sn_inv_bind/ qed-.
lemma lleq_inv_flat: ∀I,L1,L2,V,T,l. L1 ≡[ⓕ{I}V.T, l] L2 →
/2 width=4 by llpx_sn_fwd_bind_sn/ qed-.
lemma lleq_fwd_bind_dx: ∀a,I,L1,L2,V,T,l.
/2 width=4 by llpx_sn_fwd_bind_sn/ qed-.
lemma lleq_fwd_bind_dx: ∀a,I,L1,L2,V,T,l.
- L1 â\89¡[â\93\91{a,I}V.T, l] L2 â\86\92 L1.â\93\91{I}V â\89¡[T, ⫯l] L2.ⓑ{I}V.
+ L1 â\89¡[â\93\91{a,I}V.T, l] L2 â\86\92 L1.â\93\91{I}V â\89¡[T, â\86\91l] L2.ⓑ{I}V.
/2 width=2 by llpx_sn_fwd_bind_dx/ qed-.
lemma lleq_fwd_flat_sn: ∀I,L1,L2,V,T,l.
/2 width=2 by llpx_sn_fwd_bind_dx/ qed-.
lemma lleq_fwd_flat_sn: ∀I,L1,L2,V,T,l.
/2 width=1 by llpx_sn_gref/ qed.
lemma lleq_bind: ∀a,I,L1,L2,V,T,l.
/2 width=1 by llpx_sn_gref/ qed.
lemma lleq_bind: ∀a,I,L1,L2,V,T,l.