-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©.