-lemma fqus_inv_bind1: â\88\80b,p,I,G1,G2,L1,L2,V1,T1,T2. â¦\83G1,L1,â\93\91{p,I}V1.T1â¦\84 â¬\82*[b] â¦\83G2,L2,T2â¦\84 →
- ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ{p,I}V1.T1 = T2
- | â¦\83G1,L1,V1â¦\84 â¬\82*[b] â¦\83G2,L2,T2â¦\84
- | â\88§â\88§ â¦\83G1,L1.â\93\91{I}V1,T1â¦\84 â¬\82*[b] â¦\83G2,L2,T2â¦\84 & b = Ⓣ
- | â\88§â\88§ â¦\83G1,L1.â\93§,T1â¦\84 â¬\82*[b] â¦\83G2,L2,T2â¦\84 & b = Ⓕ
- | â\88\83â\88\83J,L,T. â¦\83G1,L,Tâ¦\84 â¬\82*[b] â¦\83G2,L2,T2â¦\84 & â\87§*[1] T â\89\98 â\93\91{p,I}V1.T1 & L1 = L.â\93\98{J}.
+lemma fqus_inv_bind1: â\88\80b,p,I,G1,G2,L1,L2,V1,T1,T2. â\9d¨G1,L1,â\93\91[p,I]V1.T1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© →
+ ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ[p,I]V1.T1 = T2
+ | â\9d¨G1,L1,V1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d©
+ | â\88§â\88§ â\9d¨G1,L1.â\93\91[I]V1,T1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© & b = Ⓣ
+ | â\88§â\88§ â\9d¨G1,L1.â\93§,T1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© & b = Ⓕ
+ | â\88\83â\88\83J,L,T. â\9d¨G1,L,Tâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© & â\87§[1] T â\89\98 â\93\91[p,I]V1.T1 & L1 = L.â\93\98[J].