-lemma fqup_drops_strap1: â\88\80b,G1,G2,L1,K1,K2,T1,T2,U1,i. â¬\87*[i] L1 â\89\98 K1 â\86\92 â¬\86*[i] T1 ≘ U1 →
- â¦\83G1,K1,T1â¦\84 â¬\82[b] â¦\83G2,K2,T2â¦\84 â\86\92 â¦\83G1,L1,U1â¦\84 â¬\82+[b] â¦\83G2,K2,T2â¦\84.
+lemma fqup_drops_strap1: â\88\80b,G1,G2,L1,K1,K2,T1,T2,U1,i. â\87©*[i] L1 â\89\98 K1 â\86\92 â\87§*[i] T1 ≘ U1 →
+ â\9dªG1,K1,T1â\9d« â¬\82[b] â\9dªG2,K2,T2â\9d« â\86\92 â\9dªG1,L1,U1â\9d« â¬\82+[b] â\9dªG2,K2,T2â\9d«.