-lemma fqus_inv_bind1_true: â\88\80p,I,G1,G2,L1,L2,V1,T1,T2. â¦\83G1,L1,â\93\91{p,I}V1.T1â¦\84 â\8a\90* â¦\83G2,L2,T2â¦\84 →
- ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ{p,I}V1.T1 = T2
- | â¦\83G1,L1,V1â¦\84 â\8a\90* â¦\83G2,L2,T2â¦\84
- | â¦\83G1,L1.â\93\91{I}V1,T1â¦\84 â\8a\90* â¦\83G2,L2,T2â¦\84
- | â\88\83â\88\83J,L,T. â¦\83G1,L,Tâ¦\84 â\8a\90* â¦\83G2,L2,T2â¦\84 & â¬\86*[1] T â\89\98 â\93\91{p,I}V1.T1 & L1 = L.â\93\98{J}.
-#p #I #G1 #G2 #L1 #L2 #V1 #T1 #T2 #H elim (fqus_inv_bind1 … H) -H [1,4: * ]
-/3 width=1 by and3_intro, or4_intro0, or4_intro1, or4_intro2, or4_intro3, ex3_3_intro/
+lemma fqus_inv_bind1_true: â\88\80p,I,G1,G2,L1,L2,V1,T1,T2. â\9d¨G1,L1,â\93\91[p,I]V1.T1â\9d© â¬\82* â\9d¨G2,L2,T2â\9d© →
+ ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ[p,I]V1.T1 = T2
+ | â\9d¨G1,L1,V1â\9d© â¬\82* â\9d¨G2,L2,T2â\9d©
+ | â\9d¨G1,L1.â\93\91[I]V1,T1â\9d© â¬\82* â\9d¨G2,L2,T2â\9d©
+ | â\88\83â\88\83J,L,T. â\9d¨G1,L,Tâ\9d© â¬\82* â\9d¨G2,L2,T2â\9d© & â\87§[1] T â\89\98 â\93\91[p,I]V1.T1 & L1 = L.â\93\98[J].
+#p #I #G1 #G2 #L1 #L2 #V1 #T1 #T2 #H elim (fqus_inv_bind1 … H) -H [1,3,4: * ]
+/3 width=1 by and3_intro, or4_intro0, or4_intro1, or4_intro2, or4_intro3/