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