update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / s_computation / fqus.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqus.ma b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqus.ma
index 3a58ae745433cb01d2e55f787bf89865e05a13cd..490e8e8a9101725d73b960a52e0165d2f6e8a1cf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqus.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqus.ma
@@ -34,15 +34,15 @@ interpretation "star-iterated structural successor (closure)"
 (* Basic eliminators ********************************************************)
 
 lemma fqus_ind: ∀b,G1,L1,T1. ∀Q:relation3 …. Q G1 L1 T1 →
-                (â\88\80G,G2,L,L2,T,T2. â\9dªG1,L1,T1â\9d« â¬\82*[b] â\9dªG,L,Tâ\9d« â\86\92 â\9dªG,L,Tâ\9d« â¬\82⸮[b] â\9dªG2,L2,T2â\9d« → Q G L T → Q G2 L2 T2) →
-                â\88\80G2,L2,T2. â\9dªG1,L1,T1â\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« → Q G2 L2 T2.
+                (â\88\80G,G2,L,L2,T,T2. â\9d¨G1,L1,T1â\9d© â¬\82*[b] â\9d¨G,L,Tâ\9d© â\86\92 â\9d¨G,L,Tâ\9d© â¬\82⸮[b] â\9d¨G2,L2,T2â\9d© → Q G L T → Q G2 L2 T2) →
+                â\88\80G2,L2,T2. â\9d¨G1,L1,T1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© → Q G2 L2 T2.
 #b #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
 @(tri_TC_star_ind … IH1 IH2 G2 L2 T2 H) //
 qed-.
 
 lemma fqus_ind_dx: ∀b,G2,L2,T2. ∀Q:relation3 …. Q G2 L2 T2 →
-                   (â\88\80G1,G,L1,L,T1,T. â\9dªG1,L1,T1â\9d« â¬\82⸮[b] â\9dªG,L,Tâ\9d« â\86\92 â\9dªG,L,Tâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« → Q G L T → Q G1 L1 T1) →
-                   â\88\80G1,L1,T1. â\9dªG1,L1,T1â\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« → Q G1 L1 T1.
+                   (â\88\80G1,G,L1,L,T1,T. â\9d¨G1,L1,T1â\9d© â¬\82⸮[b] â\9d¨G,L,Tâ\9d© â\86\92 â\9d¨G,L,Tâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© → Q G L T → Q G1 L1 T1) →
+                   â\88\80G1,L1,T1. â\9d¨G1,L1,T1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© → Q G1 L1 T1.
 #b #G2 #L2 #T2 #Q #IH1 #IH2 #G1 #L1 #T1 #H
 @(tri_TC_star_ind_dx … IH1 IH2 G1 L1 T1 H) //
 qed-.
@@ -52,56 +52,56 @@ qed-.
 lemma fqus_refl: ∀b. tri_reflexive … (fqus b).
 /2 width=1 by tri_inj/ qed.
 
-lemma fquq_fqus: â\88\80b,G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â¬\82⸮[b] â\9dªG2,L2,T2â\9d« →
-                 â\9dªG1,L1,T1â\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d«.
+lemma fquq_fqus: â\88\80b,G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82⸮[b] â\9d¨G2,L2,T2â\9d© →
+                 â\9d¨G1,L1,T1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d©.
 /2 width=1 by tri_inj/ qed.
 
-lemma fqus_strap1: â\88\80b,G1,G,G2,L1,L,L2,T1,T,T2. â\9dªG1,L1,T1â\9d« â¬\82*[b] â\9dªG,L,Tâ\9d« →
-                   â\9dªG,L,Tâ\9d« â¬\82⸮[b] â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d«.
+lemma fqus_strap1: â\88\80b,G1,G,G2,L1,L,L2,T1,T,T2. â\9d¨G1,L1,T1â\9d© â¬\82*[b] â\9d¨G,L,Tâ\9d© →
+                   â\9d¨G,L,Tâ\9d© â¬\82⸮[b] â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d©.
 /2 width=5 by tri_step/ qed-.
 
-lemma fqus_strap2: â\88\80b,G1,G,G2,L1,L,L2,T1,T,T2. â\9dªG1,L1,T1â\9d« â¬\82⸮[b] â\9dªG,L,Tâ\9d« →
-                   â\9dªG,L,Tâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d«.
+lemma fqus_strap2: â\88\80b,G1,G,G2,L1,L,L2,T1,T,T2. â\9d¨G1,L1,T1â\9d© â¬\82⸮[b] â\9d¨G,L,Tâ\9d© →
+                   â\9d¨G,L,Tâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d©.
 /2 width=5 by tri_TC_strap/ qed-.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma fqus_inv_fqu_sn: â\88\80b,G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« →
+lemma fqus_inv_fqu_sn: â\88\80b,G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© →
                        (∧∧ G1 = G2 & L1 = L2 & T1 = T2) ∨
-                       â\88\83â\88\83G,L,T. â\9dªG1,L1,T1â\9d« â¬\82[b] â\9dªG,L,Tâ\9d« & â\9dªG,L,Tâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d«.
+                       â\88\83â\88\83G,L,T. â\9d¨G1,L1,T1â\9d© â¬\82[b] â\9d¨G,L,Tâ\9d© & â\9d¨G,L,Tâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d©.
 #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 @(fqus_ind_dx … H12) -G1 -L1 -T1 /3 width=1 by and3_intro, or_introl/
 #G1 #G #L1 #L #T1 #T * /3 width=5 by ex2_3_intro, or_intror/
 * #HG #HL #HT #_ destruct //
 qed-.
 
-lemma fqus_inv_sort1: â\88\80b,G1,G2,L1,L2,T2,s. â\9dªG1,L1,â\8b\86sâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« →
+lemma fqus_inv_sort1: â\88\80b,G1,G2,L1,L2,T2,s. â\9d¨G1,L1,â\8b\86sâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© →
                       (∧∧ G1 = G2 & L1 = L2 & ⋆s = T2) ∨
-                      â\88\83â\88\83J,L. â\9dªG1,L,â\8b\86sâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« & L1 = L.ⓘ[J].
+                      â\88\83â\88\83J,L. â\9d¨G1,L,â\8b\86sâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© & L1 = L.ⓘ[J].
 #b #G1 #G2 #L1 #L2 #T2 #s #H elim (fqus_inv_fqu_sn … H) -H * /3 width=1 by and3_intro, or_introl/
 #G #L #T #H elim (fqu_inv_sort1 … H) -H /3 width=4 by ex2_2_intro, or_intror/
 qed-.
 
-lemma fqus_inv_lref1: â\88\80b,G1,G2,L1,L2,T2,i. â\9dªG1,L1,#iâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« →
+lemma fqus_inv_lref1: â\88\80b,G1,G2,L1,L2,T2,i. â\9d¨G1,L1,#iâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© →
                       ∨∨ ∧∧ G1 = G2 & L1 = L2 & #i = T2
-                       | â\88\83â\88\83J,L,V. â\9dªG1,L,Vâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« & L1 = L.ⓑ[J]V & i = 0
-                       | â\88\83â\88\83J,L,j. â\9dªG1,L,#jâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« & L1 = L.ⓘ[J] & i = ↑j.
+                       | â\88\83â\88\83J,L,V. â\9d¨G1,L,Vâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© & L1 = L.ⓑ[J]V & i = 0
+                       | â\88\83â\88\83J,L,j. â\9d¨G1,L,#jâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© & 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=6 by ex3_3_intro, or3_intro1, or3_intro2/
 qed-.
 
-lemma fqus_inv_gref1: â\88\80b,G1,G2,L1,L2,T2,l. â\9dªG1,L1,§lâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« →
+lemma fqus_inv_gref1: â\88\80b,G1,G2,L1,L2,T2,l. â\9d¨G1,L1,§lâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© →
                       (∧∧ G1 = G2 & L1 = L2 & §l = T2) ∨
-                      â\88\83â\88\83J,L. â\9dªG1,L,§lâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« & L1 = L.ⓘ[J].
+                      â\88\83â\88\83J,L. â\9d¨G1,L,§lâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© & L1 = L.ⓘ[J].
 #b #G1 #G2 #L1 #L2 #T2 #l #H elim (fqus_inv_fqu_sn … H) -H * /3 width=1 by and3_intro, or_introl/
 #G #L #T #H elim (fqu_inv_gref1 … H) -H /3 width=4 by ex2_2_intro, or_intror/
 qed-.
 
-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« →
+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« & ⇧[1] T ≘ ⓑ[p,I]V1.T1 & L1 = L.ⓘ[J].
+                       | â\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© & ⇧[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
@@ -109,21 +109,21 @@ lemma fqus_inv_bind1: ∀b,p,I,G1,G2,L1,L2,V1,T1,T2. ❪G1,L1,ⓑ[p,I]V1.T1❫ 
 qed-.
 
 
-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« →
+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« & ⇧[1] T ≘ ⓑ[p,I]V1.T1 & L1 = L.ⓘ[J].
+                               | â\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© & ⇧[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
 qed-.
 
-lemma fqus_inv_flat1: â\88\80b,I,G1,G2,L1,L2,V1,T1,T2. â\9dªG1,L1,â\93\95[I]V1.T1â\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« →
+lemma fqus_inv_flat1: â\88\80b,I,G1,G2,L1,L2,V1,T1,T2. â\9d¨G1,L1,â\93\95[I]V1.T1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© →
                       ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓕ[I]V1.T1 = T2
-                       | â\9dªG1,L1,V1â\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d«
-                       | â\9dªG1,L1,T1â\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d«
-                       | â\88\83â\88\83J,L,T. â\9dªG1,L,Tâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« & ⇧[1] T ≘ ⓕ[I]V1.T1 & L1 = L.ⓘ[J].
+                       | â\9d¨G1,L1,V1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d©
+                       | â\9d¨G1,L1,T1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d©
+                       | â\88\83â\88\83J,L,T. â\9d¨G1,L,Tâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© & ⇧[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
@@ -132,35 +132,35 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma fqus_inv_atom1: â\88\80b,I,G1,G2,L2,T2. â\9dªG1,â\8b\86,â\93ª[I]â\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« →
+lemma fqus_inv_atom1: â\88\80b,I,G1,G2,L2,T2. â\9d¨G1,â\8b\86,â\93ª[I]â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© →
                       ∧∧ G1 = G2 & ⋆ = L2 & ⓪[I] = T2.
 #b #I #G1 #G2 #L2 #T2 #H elim (fqus_inv_fqu_sn … H) -H * /2 width=1 by and3_intro/
 #G #L #T #H elim (fqu_inv_atom1 … H)
 qed-.
 
-lemma fqus_inv_sort1_bind: â\88\80b,I,G1,G2,L1,L2,T2,s. â\9dªG1,L1.â\93\98[I],â\8b\86sâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« →
-                           (â\88§â\88§ G1 = G2 & L1.â\93\98[I] = L2 & â\8b\86s = T2) â\88¨ â\9dªG1,L1,â\8b\86sâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d«.
+lemma fqus_inv_sort1_bind: â\88\80b,I,G1,G2,L1,L2,T2,s. â\9d¨G1,L1.â\93\98[I],â\8b\86sâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© →
+                           (â\88§â\88§ G1 = G2 & L1.â\93\98[I] = L2 & â\8b\86s = T2) â\88¨ â\9d¨G1,L1,â\8b\86sâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d©.
 #b #I #G1 #G2 #L1 #L2 #T2 #s #H elim (fqus_inv_fqu_sn … H) -H * /3 width=1 by and3_intro, or_introl/
 #G #L #T #H elim (fqu_inv_sort1_bind … H) -H
 #H1 #H2 #H3 #H destruct /2 width=1 by or_intror/
 qed-.
 
-lemma fqus_inv_zero1_pair: â\88\80b,I,G1,G2,L1,L2,V1,T2. â\9dªG1,L1.â\93\91[I]V1,#0â\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« →
-                           (â\88§â\88§ G1 = G2 & L1.â\93\91[I]V1 = L2 & #0 = T2) â\88¨ â\9dªG1,L1,V1â\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d«.
+lemma fqus_inv_zero1_pair: â\88\80b,I,G1,G2,L1,L2,V1,T2. â\9d¨G1,L1.â\93\91[I]V1,#0â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© →
+                           (â\88§â\88§ G1 = G2 & L1.â\93\91[I]V1 = L2 & #0 = T2) â\88¨ â\9d¨G1,L1,V1â\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d©.
 #b #I #G1 #G2 #L1 #L2 #V1 #T2 #H elim (fqus_inv_fqu_sn … H) -H * /3 width=1 by and3_intro, or_introl/
 #G #L #T #H elim (fqu_inv_zero1_pair … H) -H
 #H1 #H2 #H3 #H destruct /2 width=1 by or_intror/
 qed-.
 
-lemma fqus_inv_lref1_bind: â\88\80b,I,G1,G2,L1,L2,T2,i. â\9dªG1,L1.â\93\98[I],#â\86\91iâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« →
-                           (â\88§â\88§ G1 = G2 & L1.â\93\98[I] = L2 & #(â\86\91i) = T2) â\88¨ â\9dªG1,L1,#iâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d«.
+lemma fqus_inv_lref1_bind: â\88\80b,I,G1,G2,L1,L2,T2,i. â\9d¨G1,L1.â\93\98[I],#â\86\91iâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© →
+                           (â\88§â\88§ G1 = G2 & L1.â\93\98[I] = L2 & #(â\86\91i) = T2) â\88¨ â\9d¨G1,L1,#iâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d©.
 #b #I #G1 #G2 #L1 #L2 #T2 #i #H elim (fqus_inv_fqu_sn … H) -H * /3 width=1 by and3_intro, or_introl/
 #G #L #T #H elim (fqu_inv_lref1_bind … H) -H
 #H1 #H2 #H3 #H destruct /2 width=1 by or_intror/
 qed-.
 
-lemma fqus_inv_gref1_bind: â\88\80b,I,G1,G2,L1,L2,T2,l. â\9dªG1,L1.â\93\98[I],§lâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d« →
-                           (â\88§â\88§ G1 = G2 & L1.â\93\98[I] = L2 & §l = T2) â\88¨ â\9dªG1,L1,§lâ\9d« â¬\82*[b] â\9dªG2,L2,T2â\9d«.
+lemma fqus_inv_gref1_bind: â\88\80b,I,G1,G2,L1,L2,T2,l. â\9d¨G1,L1.â\93\98[I],§lâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© →
+                           (â\88§â\88§ G1 = G2 & L1.â\93\98[I] = L2 & §l = T2) â\88¨ â\9d¨G1,L1,§lâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d©.
 #b #I #G1 #G2 #L1 #L2 #T2 #l #H elim (fqus_inv_fqu_sn … H) -H * /3 width=1 by and3_intro, or_introl/
 #G #L #T #H elim (fqu_inv_gref1_bind … H) -H
 #H1 #H2 #H3 #H destruct /2 width=1 by or_intror/