+(* Advanced inversion lemmas ************************************************)
+
+lemma fqu_inv_atom1: ∀I,G1,G2,L2,T2. ⦃G1, ⋆, ⓪{I}⦄ ⊐ ⦃G2, L2, T2⦄ → ⊥.
+* #x #G1 #G2 #L2 #T2 #H
+[ elim (fqu_inv_sort1 … H) | elim (fqu_inv_lref1 … H) * | elim (fqu_inv_gref1 … H) ] -H
+#I #V [3: #i ] #_ #H destruct
+qed-.
+
+lemma fqu_inv_sort1_pair: ∀I,G1,G2,K,L2,V,T2,s. ⦃G1, K.ⓑ{I}V, ⋆s⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & L2 = K & T2 = ⋆s.
+#I #G1 #G2 #K #L2 #V #T2 #s #H elim (fqu_inv_sort1 … H) -H
+#Z #X #H1 #H2 #H3 destruct /2 width=1 by and3_intro/
+qed-.
+
+lemma fqu_inv_zero1_pair: ∀I,G1,G2,K,L2,V,T2. ⦃G1, K.ⓑ{I}V, #0⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & L2 = K & T2 = V.
+#I #G1 #G2 #K #L2 #V #T2 #H elim (fqu_inv_lref1 … H) -H *
+#Z #X [2: #x ] #H1 #H2 #H3 #H4 destruct /2 width=1 by and3_intro/
+qed-.
+
+lemma fqu_inv_lref1_pair: ∀I,G1,G2,K,L2,V,T2,i. ⦃G1, K.ⓑ{I}V, #(⫯i)⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & L2 = K & T2 = #i.
+#I #G1 #G2 #K #L2 #V #T2 #i #H elim (fqu_inv_lref1 … H) -H *
+#Z #X [2: #x ] #H1 #H2 #H3 #H4 destruct /2 width=1 by and3_intro/
+qed-.
+
+lemma fqu_inv_gref1_pair: ∀I,G1,G2,K,L2,V,T2,l. ⦃G1, K.ⓑ{I}V, §l⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & L2 = K & T2 = §l.
+#I #G1 #G2 #K #L2 #V #T2 #l #H elim (fqu_inv_gref1 … H) -H
+#Z #X #H1 #H2 #H3 destruct /2 width=1 by and3_intro/
+qed-.
+