(* *)
(**************************************************************************)
+include "ground_2/xoa/ex_2_3.ma".
+include "ground_2/xoa/ex_3_3.ma".
+include "ground_2/xoa/or_5.ma".
include "ground_2/lib/star.ma".
include "static_2/notation/relations/suptermstar_6.ma".
include "static_2/notation/relations/suptermstar_7.ma".
| ∃∃J,L,V. ⦃G1,L,V⦄ ⬂*[b] ⦃G2,L2,T2⦄ & L1 = L.ⓑ{J}V & i = 0
| ∃∃J,L,j. ⦃G1,L,#j⦄ ⬂*[b] ⦃G2,L2,T2⦄ & L1 = L.ⓘ{J} & i = ↑j.
#b #G1 #G2 #L1 #L2 #T2 #i #H elim (fqus_inv_fqu_sn … H) -H * /3 width=1 by and3_intro, or3_intro0/
-#G #L #T #H elim (fqu_inv_lref1 … H) -H * /3 width=7 by or3_intro1, or3_intro2, ex3_4_intro, ex3_3_intro/
+#G #L #T #H elim (fqu_inv_lref1 … H) -H * /3 width=6 by ex3_3_intro, or3_intro1, or3_intro2/
qed-.
lemma fqus_inv_gref1: ∀b,G1,G2,L1,L2,T2,l. ⦃G1,L1,§l⦄ ⬂*[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⦄
- | ∧∧ ⦃G1,L1.ⓑ{I}V1,T1⦄ ⬂*[b] ⦃G2,L2,T2⦄ & b = Ⓣ
+ | ∧∧ ⦃G1,L1.ⓑ{I}V1,T1⦄ ⬂*[b] ⦃G2,L2,T2⦄ & b = Ⓣ
| ∧∧ ⦃G1,L1.ⓧ,T1⦄ ⬂*[b] ⦃G2,L2,T2⦄ & b = Ⓕ
- | â\88\83â\88\83J,L,T. â¦\83G1,L,Tâ¦\84 â¬\82*[b] â¦\83G2,L2,T2â¦\84 & â¬\86*[1] T ≘ ⓑ{p,I}V1.T1 & L1 = L.ⓘ{J}.
+ | â\88\83â\88\83J,L,T. â¦\83G1,L,Tâ¦\84 â¬\82*[b] â¦\83G2,L2,T2â¦\84 & â\87§*[1] T ≘ ⓑ{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 [3,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 â¬\82* â¦\83G2,L2,T2â¦\84 & â¬\86*[1] T ≘ ⓑ{p,I}V1.T1 & L1 = L.ⓘ{J}.
+ | â\88\83â\88\83J,L,T. â¦\83G1,L,Tâ¦\84 â¬\82* â¦\83G2,L2,T2â¦\84 & â\87§*[1] T ≘ ⓑ{p,I}V1.T1 & L1 = L.ⓘ{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/
#_ #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 â¬\82*[b] â¦\83G2,L2,T2â¦\84 & â¬\86*[1] T ≘ ⓕ{I}V1.T1 & L1 = L.ⓘ{J}.
+ | â\88\83â\88\83J,L,T. â¦\83G1,L,Tâ¦\84 â¬\82*[b] â¦\83G2,L2,T2â¦\84 & â\87§*[1] T ≘ ⓕ{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