more additions and corrections for the article

[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 1289e8487587df00115ccd5468e4778622cd40d6..d1183daff751761d5b9dc82127d237223f3bb4a6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqus.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqus.ma
@@ -31,15 +31,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. â¦\83G1,L1,T1â¦\84 â\8a\90*[b] â¦\83G,L,Tâ¦\84 â\86\92 â¦\83G,L,Tâ¦\84 â\8a\90⸮[b] ⦃G2,L2,T2⦄ → Q G L T → Q G2 L2 T2) →
-                â\88\80G2,L2,T2. â¦\83G1,L1,T1â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ → Q G2 L2 T2.
+                (â\88\80G,G2,L,L2,T,T2. â¦\83G1,L1,T1â¦\84 â¬\82*[b] â¦\83G,L,Tâ¦\84 â\86\92 â¦\83G,L,Tâ¦\84 â¬\82⸮[b] ⦃G2,L2,T2⦄ → Q G L T → Q G2 L2 T2) →
+                â\88\80G2,L2,T2. â¦\83G1,L1,T1â¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ → 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. â¦\83G1,L1,T1â¦\84 â\8a\90⸮[b] â¦\83G,L,Tâ¦\84 â\86\92 â¦\83G,L,Tâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ → Q G L T → Q G1 L1 T1) →
-                   â\88\80G1,L1,T1. â¦\83G1,L1,T1â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ → Q G1 L1 T1.
+                   (â\88\80G1,G,L1,L,T1,T. â¦\83G1,L1,T1â¦\84 â¬\82⸮[b] â¦\83G,L,Tâ¦\84 â\86\92 â¦\83G,L,Tâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ → Q G L T → Q G1 L1 T1) →
+                   â\88\80G1,L1,T1. â¦\83G1,L1,T1â¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ → 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-.
@@ -49,78 +49,78 @@ 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. â¦\83G1,L1,T1â¦\84 â\8a\90⸮[b] ⦃G2,L2,T2⦄ →
-                 â¦\83G1,L1,T1â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄.
+lemma fquq_fqus: â\88\80b,G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â¬\82⸮[b] ⦃G2,L2,T2⦄ →
+                 â¦\83G1,L1,T1â¦\84 â¬\82*[b] ⦃G2,L2,T2⦄.
 /2 width=1 by tri_inj/ qed.
 
-lemma fqus_strap1: â\88\80b,G1,G,G2,L1,L,L2,T1,T,T2. â¦\83G1,L1,T1â¦\84 â\8a\90*[b] ⦃G,L,T⦄ →
-                   â¦\83G,L,Tâ¦\84 â\8a\90⸮[b] â¦\83G2,L2,T2â¦\84 â\86\92 â¦\83G1,L1,T1â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄.
+lemma fqus_strap1: â\88\80b,G1,G,G2,L1,L,L2,T1,T,T2. â¦\83G1,L1,T1â¦\84 â¬\82*[b] ⦃G,L,T⦄ →
+                   â¦\83G,L,Tâ¦\84 â¬\82⸮[b] â¦\83G2,L2,T2â¦\84 â\86\92 â¦\83G1,L1,T1â¦\84 â¬\82*[b] ⦃G2,L2,T2⦄.
 /2 width=5 by tri_step/ qed-.
 
-lemma fqus_strap2: â\88\80b,G1,G,G2,L1,L,L2,T1,T,T2. â¦\83G1,L1,T1â¦\84 â\8a\90⸮[b] ⦃G,L,T⦄ →
-                   â¦\83G,L,Tâ¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 â\86\92 â¦\83G1,L1,T1â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄.
+lemma fqus_strap2: â\88\80b,G1,G,G2,L1,L,L2,T1,T,T2. â¦\83G1,L1,T1â¦\84 â¬\82⸮[b] ⦃G,L,T⦄ →
+                   â¦\83G,L,Tâ¦\84 â¬\82*[b] â¦\83G2,L2,T2â¦\84 â\86\92 â¦\83G1,L1,T1â¦\84 â¬\82*[b] ⦃G2,L2,T2⦄.
 /2 width=5 by tri_TC_strap/ qed-.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma fqus_inv_fqu_sn: â\88\80b,G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ →
+lemma fqus_inv_fqu_sn: â\88\80b,G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ →
                        (∧∧ G1 = G2 & L1 = L2 & T1 = T2) ∨
-                       â\88\83â\88\83G,L,T. â¦\83G1,L1,T1â¦\84 â\8a\90[b] â¦\83G,L,Tâ¦\84 & â¦\83G,L,Tâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄.
+                       â\88\83â\88\83G,L,T. â¦\83G1,L1,T1â¦\84 â¬\82[b] â¦\83G,L,Tâ¦\84 & â¦\83G,L,Tâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄.
 #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. â¦\83G1,L1,â\8b\86sâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ →
+lemma fqus_inv_sort1: â\88\80b,G1,G2,L1,L2,T2,s. â¦\83G1,L1,â\8b\86sâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ →
                       (∧∧ G1 = G2 & L1 = L2 & ⋆s = T2) ∨
-                      â\88\83â\88\83J,L. â¦\83G1,L,â\8b\86sâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ & L1 = L.ⓘ{J}.
+                      â\88\83â\88\83J,L. â¦\83G1,L,â\8b\86sâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ & 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. â¦\83G1,L1,#iâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ →
+lemma fqus_inv_lref1: â\88\80b,G1,G2,L1,L2,T2,i. â¦\83G1,L1,#iâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ →
                       ∨∨ ∧∧ G1 = G2 & L1 = L2 & #i = T2
-                       | â\88\83â\88\83J,L,V. â¦\83G1,L,Vâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ & L1 = L.ⓑ{J}V & i = 0
-                       | â\88\83â\88\83J,L,j. â¦\83G1,L,#jâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ & L1 = L.ⓘ{J} & i = ↑j.
+                       | â\88\83â\88\83J,L,V. â¦\83G1,L,Vâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ & L1 = L.ⓑ{J}V & i = 0
+                       | â\88\83â\88\83J,L,j. â¦\83G1,L,#jâ¦\84 â¬\82*[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/
 qed-.
 
-lemma fqus_inv_gref1: â\88\80b,G1,G2,L1,L2,T2,l. â¦\83G1,L1,§lâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ →
+lemma fqus_inv_gref1: â\88\80b,G1,G2,L1,L2,T2,l. â¦\83G1,L1,§lâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ →
                       (∧∧ G1 = G2 & L1 = L2 & §l = T2) ∨
-                      â\88\83â\88\83J,L. â¦\83G1,L,§lâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ & L1 = L.ⓘ{J}.
+                      â\88\83â\88\83J,L. â¦\83G1,L,§lâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ & 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. â¦\83G1,L1,â\93\91{p,I}V1.T1â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ →
+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] ⦃G2,L2,T2⦄ →
                       ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ{p,I}V1.T1 = T2
-                       | â¦\83G1,L1,V1â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄
-                       | â¦\83G1,L1.â\93\91{I}V1,T1â¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84
-                       | â¦\83G1,L1.â\93§,T1â¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 â\88§ b = Ⓕ
-                       | â\88\83â\88\83J,L,T. â¦\83G1,L,Tâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ & ⬆*[1] T ≘ ⓑ{p,I}V1.T1 & L1 = L.ⓘ{J}.
+                       | â¦\83G1,L1,V1â¦\84 â¬\82*[b] ⦃G2,L2,T2⦄
+                       | â\88§â\88§ â¦\83G1,L1.â\93\91{I}V1,T1â¦\84 â¬\82*[b] â¦\83G2,L2,T2â¦\84 & b = â\93\89 
+                       | â\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] ⦃G2,L2,T2⦄ & ⬆*[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 [4: #Hb ] #H destruct
+[4: #J ] #H1 #H2 #H3 [3,4: #Hb ] #H destruct
 /3 width=6 by or5_intro1, or5_intro2, or5_intro3, or5_intro4, ex3_3_intro, conj/
 qed-.
 
 
-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* ⦃G2,L2,T2⦄ →
+lemma fqus_inv_bind1_true: â\88\80p,I,G1,G2,L1,L2,V1,T1,T2. â¦\83G1,L1,â\93\91{p,I}V1.T1â¦\84 â¬\82* ⦃G2,L2,T2⦄ →
                            ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ{p,I}V1.T1 = T2
-                               | â¦\83G1,L1,V1â¦\84 â\8a\90* ⦃G2,L2,T2⦄
-                               | â¦\83G1,L1.â\93\91{I}V1,T1â¦\84 â\8a\90* ⦃G2,L2,T2⦄
-                               | â\88\83â\88\83J,L,T. â¦\83G1,L,Tâ¦\84 â\8a\90* ⦃G2,L2,T2⦄ & ⬆*[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,4: * ]
-/3 width=1 by and3_intro, or4_intro0, or4_intro1, or4_intro2, or4_intro3, ex3_3_intro/
+                               | â¦\83G1,L1,V1â¦\84 â¬\82* ⦃G2,L2,T2⦄
+                               | â¦\83G1,L1.â\93\91{I}V1,T1â¦\84 â¬\82* ⦃G2,L2,T2⦄
+                               | â\88\83â\88\83J,L,T. â¦\83G1,L,Tâ¦\84 â¬\82* ⦃G2,L2,T2⦄ & ⬆*[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. â¦\83G1,L1,â\93\95{I}V1.T1â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ →
+lemma fqus_inv_flat1: â\88\80b,I,G1,G2,L1,L2,V1,T1,T2. â¦\83G1,L1,â\93\95{I}V1.T1â¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ →
                       ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓕ{I}V1.T1 = T2
-                       | â¦\83G1,L1,V1â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄
-                       | â¦\83G1,L1,T1â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄
-                       | â\88\83â\88\83J,L,T. â¦\83G1,L,Tâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ & ⬆*[1] T ≘ ⓕ{I}V1.T1 & L1 = L.ⓘ{J}.
+                       | â¦\83G1,L1,V1â¦\84 â¬\82*[b] ⦃G2,L2,T2⦄
+                       | â¦\83G1,L1,T1â¦\84 â¬\82*[b] ⦃G2,L2,T2⦄
+                       | â\88\83â\88\83J,L,T. â¦\83G1,L,Tâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ & ⬆*[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
@@ -129,35 +129,35 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma fqus_inv_atom1: â\88\80b,I,G1,G2,L2,T2. â¦\83G1,â\8b\86,â\93ª{I}â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ →
+lemma fqus_inv_atom1: â\88\80b,I,G1,G2,L2,T2. â¦\83G1,â\8b\86,â\93ª{I}â¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ →
                       ∧∧ 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. â¦\83G1,L1.â\93\98{I},â\8b\86sâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ →
-                           (â\88§â\88§ G1 = G2 & L1.â\93\98{I} = L2 & â\8b\86s = T2) â\88¨ â¦\83G1,L1,â\8b\86sâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄.
+lemma fqus_inv_sort1_bind: â\88\80b,I,G1,G2,L1,L2,T2,s. â¦\83G1,L1.â\93\98{I},â\8b\86sâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ →
+                           (â\88§â\88§ G1 = G2 & L1.â\93\98{I} = L2 & â\8b\86s = T2) â\88¨ â¦\83G1,L1,â\8b\86sâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄.
 #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. â¦\83G1,L1.â\93\91{I}V1,#0â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ →
-                           (â\88§â\88§ G1 = G2 & L1.â\93\91{I}V1 = L2 & #0 = T2) â\88¨ â¦\83G1,L1,V1â¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄.
+lemma fqus_inv_zero1_pair: â\88\80b,I,G1,G2,L1,L2,V1,T2. â¦\83G1,L1.â\93\91{I}V1,#0â¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ →
+                           (â\88§â\88§ G1 = G2 & L1.â\93\91{I}V1 = L2 & #0 = T2) â\88¨ â¦\83G1,L1,V1â¦\84 â¬\82*[b] ⦃G2,L2,T2⦄.
 #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. â¦\83G1,L1.â\93\98{I},#â\86\91iâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ →
-                           (â\88§â\88§ G1 = G2 & L1.â\93\98{I} = L2 & #(â\86\91i) = T2) â\88¨ â¦\83G1,L1,#iâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄.
+lemma fqus_inv_lref1_bind: â\88\80b,I,G1,G2,L1,L2,T2,i. â¦\83G1,L1.â\93\98{I},#â\86\91iâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ →
+                           (â\88§â\88§ G1 = G2 & L1.â\93\98{I} = L2 & #(â\86\91i) = T2) â\88¨ â¦\83G1,L1,#iâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄.
 #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. â¦\83G1,L1.â\93\98{I},§lâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄ →
-                           (â\88§â\88§ G1 = G2 & L1.â\93\98{I} = L2 & §l = T2) â\88¨ â¦\83G1,L1,§lâ¦\84 â\8a\90*[b] ⦃G2,L2,T2⦄.
+lemma fqus_inv_gref1_bind: â\88\80b,I,G1,G2,L1,L2,T2,l. â¦\83G1,L1.â\93\98{I},§lâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄ →
+                           (â\88§â\88§ G1 = G2 & L1.â\93\98{I} = L2 & §l = T2) â\88¨ â¦\83G1,L1,§lâ¦\84 â¬\82*[b] ⦃G2,L2,T2⦄.
 #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/