#h #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 * -T2
/4 width=7 by cpx_cpxs, cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/
qed.
lemma cpxs_theta_dx: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2.
#h #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 * -T2
/4 width=7 by cpx_cpxs, cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/
qed.
lemma cpxs_theta_dx: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2.