-theorem fsupqa_inv_fsupq: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃⊃⸮ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄.
-#L1 #L2 #T1 #T2 #H elim H -H /2 width=1/
-* #H1 #H2 destruct //
+theorem fsupqa_inv_fsupq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H /2 width=1/
+* #H1 #H2 #H3 destruct //