-lemma cnv_fquq_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
- ⦃G1, L1⦄ ⊢ T1 ![a, h] → ⦃G2, L2⦄ ⊢ T2 ![a, h].
+lemma cnv_fquq_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⊐⸮ ⦃G2,L2,T2⦄ →
+ ⦃G1,L1⦄ ⊢ T1 ![a,h] → ⦃G2,L2⦄ ⊢ T2 ![a,h].