| ⦃G1, L1, V1⦄ ⊐*[b] ⦃G2, L2, T2⦄
| ⦃G1, L1.ⓑ{I}V1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄
| ⦃G1, L1.ⓧ, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ ∧ b = Ⓕ
- | â\88\83â\88\83J,L,T. â¦\83G1, L, Tâ¦\84 â\8a\90*[b] â¦\83G2, L2, T2â¦\84 & â¬\86*[1] T â\89¡ ⓑ{p,I}V1.T1 & L1 = L.ⓘ{J}.
+ | â\88\83â\88\83J,L,T. â¦\83G1, L, Tâ¦\84 â\8a\90*[b] â¦\83G2, L2, T2â¦\84 & â¬\86*[1] T â\89\98 ⓑ{p,I}V1.T1 & L1 = L.ⓘ{J}.
#b #p #I #G1 #G2 #L1 #L2 #V1 #T1 #T2 #H elim (fqus_inv_fqu_sn … H) -H * /3 width=1 by and3_intro, or5_intro0/
#G #L #T #H elim (fqu_inv_bind1 … H) -H *
[4: #J ] #H1 #H2 #H3 [4: #Hb ] #H destruct
∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ{p,I}V1.T1 = T2
| ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄
| ⦃G1, L1.ⓑ{I}V1, T1⦄ ⊐* ⦃G2, L2, T2⦄
- | â\88\83â\88\83J,L,T. â¦\83G1, L, Tâ¦\84 â\8a\90* â¦\83G2, L2, T2â¦\84 & â¬\86*[1] T â\89¡ ⓑ{p,I}V1.T1 & L1 = L.ⓘ{J}.
+ | â\88\83â\88\83J,L,T. â¦\83G1, L, Tâ¦\84 â\8a\90* â¦\83G2, L2, T2â¦\84 & â¬\86*[1] T â\89\98 ⓑ{p,I}V1.T1 & L1 = L.ⓘ{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/
#_ #H destruct
∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓕ{I}V1.T1 = T2
| ⦃G1, L1, V1⦄ ⊐*[b] ⦃G2, L2, T2⦄
| ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄
- | â\88\83â\88\83J,L,T. â¦\83G1, L, Tâ¦\84 â\8a\90*[b] â¦\83G2, L2, T2â¦\84 & â¬\86*[1] T â\89¡ ⓕ{I}V1.T1 & L1 = L.ⓘ{J}.
+ | â\88\83â\88\83J,L,T. â¦\83G1, L, Tâ¦\84 â\8a\90*[b] â¦\83G2, L2, T2â¦\84 & â¬\86*[1] T â\89\98 ⓕ{I}V1.T1 & L1 = L.ⓘ{J}.
#b #I #G1 #G2 #L1 #L2 #V1 #T1 #T2 #H elim (fqus_inv_fqu_sn … H) -H * /3 width=1 by and3_intro, or4_intro0/
#G #L #T #H elim (fqu_inv_flat1 … H) -H *
[3: #J ] #H1 #H2 #H3 #H destruct