(* *)
(**************************************************************************)
-include "ground_2/lib/star.ma".
+include "ground/xoa/ex_2_3.ma".
+include "ground/xoa/ex_3_3.ma".
+include "ground/xoa/or_5.ma".
+include "ground/lib/star.ma".
include "static_2/notation/relations/suptermstar_6.ma".
include "static_2/notation/relations/suptermstar_7.ma".
include "static_2/s_transition/fquq.ma".
(* 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] â¦\83G2,L2,T2â¦\84 → Q G L T → Q G2 L2 T2) →
- â\88\80G2,L2,T2. â¦\83G1,L1,T1â¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 → 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. â¦\83G1,L1,T1â¦\84 â\8a\90⸮[b] â¦\83G,L,Tâ¦\84 â\86\92 â¦\83G,L,Tâ¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 → Q G L T → Q G1 L1 T1) →
- â\88\80G1,L1,T1. â¦\83G1,L1,T1â¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 → 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-.
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] â¦\83G2,L2,T2â¦\84 →
- â¦\83G1,L1,T1â¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84.
+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. â¦\83G1,L1,T1â¦\84 â\8a\90*[b] â¦\83G,L,Tâ¦\84 →
- â¦\83G,L,Tâ¦\84 â\8a\90⸮[b] â¦\83G2,L2,T2â¦\84 â\86\92 â¦\83G1,L1,T1â¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84.
+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. â¦\83G1,L1,T1â¦\84 â\8a\90⸮[b] â¦\83G,L,Tâ¦\84 →
- â¦\83G,L,Tâ¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 â\86\92 â¦\83G1,L1,T1â¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84.
+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. â¦\83G1,L1,T1â¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 →
+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. â¦\83G1,L1,T1â¦\84 â\8a\90[b] â¦\83G,L,Tâ¦\84 & â¦\83G,L,Tâ¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84.
+ â\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. â¦\83G1,L1,â\8b\86sâ¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 →
+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. â¦\83G1,L,â\8b\86sâ¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 & L1 = L.â\93\98{J}.
+ â\88\83â\88\83J,L. â\9d¨G1,L,â\8b\86sâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© & L1 = L.â\93\98[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] â¦\83G2,L2,T2â¦\84 →
+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. â¦\83G1,L,Vâ¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 & L1 = L.â\93\91{J}V & i = 0
- | â\88\83â\88\83J,L,j. â¦\83G1,L,#jâ¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 & L1 = L.â\93\98{J} & i = ↑j.
+ | â\88\83â\88\83J,L,V. â\9d¨G1,L,Vâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© & L1 = L.â\93\91[J]V & i = 0
+ | â\88\83â\88\83J,L,j. â\9d¨G1,L,#jâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© & L1 = L.â\93\98[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: â\88\80b,G1,G2,L1,L2,T2,l. â¦\83G1,L1,§lâ¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 →
+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. â¦\83G1,L,§lâ¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 & L1 = L.â\93\98{J}.
+ â\88\83â\88\83J,L. â\9d¨G1,L,§lâ\9d© â¬\82*[b] â\9d¨G2,L2,T2â\9d© & L1 = L.â\93\98[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] â¦\83G2,L2,T2â¦\84 →
- ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ{p,I}V1.T1 = T2
- | â¦\83G1,L1,V1â¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84
- | â¦\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] â¦\83G2,L2,T2â¦\84 & â¬\86*[1] T â\89\98 â\93\91{p,I}V1.T1 & L1 = L.â\93\98{J}.
+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 = â\93\89
+ | â\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© & â\87§[1] T â\89\98 â\93\91[p,I]V1.T1 & L1 = L.â\93\98[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* â¦\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/
#_ #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] â¦\83G2,L2,T2â¦\84 →
- ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓕ{I}V1.T1 = T2
- | â¦\83G1,L1,V1â¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84
- | â¦\83G1,L1,T1â¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84
- | â\88\83â\88\83J,L,T. â¦\83G1,L,Tâ¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 & â¬\86*[1] T â\89\98 â\93\95{I}V1.T1 & L1 = L.â\93\98{J}.
+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© & â\87§[1] T â\89\98 â\93\95[I]V1.T1 & L1 = L.â\93\98[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
(* Advanced inversion lemmas ************************************************)
-lemma fqus_inv_atom1: â\88\80b,I,G1,G2,L2,T2. â¦\83G1,â\8b\86,â\93ª{I}â¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 →
- ∧∧ G1 = G2 & ⋆ = L2 & ⓪{I} = T2.
+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. â¦\83G1,L1.â\93\98{I},â\8b\86sâ¦\84 â\8a\90*[b] â¦\83G2,L2,T2â¦\84 →
- (∧∧ G1 = G2 & L1.ⓘ{I} = L2 & ⋆s = T2) ∨ ⦃G1,L1,⋆s⦄ ⊐*[b] ⦃G2,L2,T2⦄.
+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© →
+ (∧∧ G1 = G2 & L1.ⓘ[I] = L2 & ⋆s = T2) ∨ ❨G1,L1,⋆s❩ ⬂*[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] â¦\83G2,L2,T2â¦\84 →
- (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & #0 = T2) ∨ ⦃G1,L1,V1⦄ ⊐*[b] ⦃G2,L2,T2⦄.
+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© →
+ (∧∧ G1 = G2 & L1.ⓑ[I]V1 = L2 & #0 = T2) ∨ ❨G1,L1,V1❩ ⬂*[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] â¦\83G2,L2,T2â¦\84 →
- (∧∧ G1 = G2 & L1.ⓘ{I} = L2 & #(↑i) = T2) ∨ ⦃G1,L1,#i⦄ ⊐*[b] ⦃G2,L2,T2⦄.
+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© →
+ (∧∧ G1 = G2 & L1.ⓘ[I] = L2 & #(↑i) = T2) ∨ ❨G1,L1,#i❩ ⬂*[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] â¦\83G2,L2,T2â¦\84 →
- (∧∧ G1 = G2 & L1.ⓘ{I} = L2 & §l = T2) ∨ ⦃G1,L1,§l⦄ ⊐*[b] ⦃G2,L2,T2⦄.
+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© →
+ (∧∧ G1 = G2 & L1.ⓘ[I] = L2 & §l = T2) ∨ ❨G1,L1,§l❩ ⬂*[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/