lemma fqus_inv_bind1: ∀b,p,I,G1,G2,L1,L2,V1,T1,T2. ⦃G1,L1,ⓑ{p,I}V1.T1⦄ ⬂*[b] ⦃G2,L2,T2⦄ →
∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ{p,I}V1.T1 = T2
| ⦃G1,L1,V1⦄ ⬂*[b] ⦃G2,L2,T2⦄
lemma fqus_inv_bind1: ∀b,p,I,G1,G2,L1,L2,V1,T1,T2. ⦃G1,L1,ⓑ{p,I}V1.T1⦄ ⬂*[b] ⦃G2,L2,T2⦄ →
∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ{p,I}V1.T1 = T2
| ⦃G1,L1,V1⦄ ⬂*[b] ⦃G2,L2,T2⦄