-fact aaa_inv_lref_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀i. T = #i →
- ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I} V & ⦃G, K⦄ ⊢ V ⁝ A.
+fact aaa_inv_zero_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → T = #0 →
+ ∃∃I,K,V. L = K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ⁝ A.
+#G #L #T #A * -G -L -T -A /2 width=5 by ex2_3_intro/
+[ #G #L #s #H destruct
+| #I #G #L #V #A #i #_ #H destruct
+| #p #G #L #V #T #B #A #_ #_ #H destruct
+| #p #G #L #V #T #B #A #_ #_ #H destruct
+| #G #L #V #T #B #A #_ #_ #H destruct
+| #G #L #V #T #A #_ #_ #H destruct
+]
+qed-.
+
+lemma aaa_inv_zero: ∀G,L,A. ⦃G, L⦄ ⊢ #0 ⁝ A →
+ ∃∃I,K,V. L = K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ⁝ A.
+/2 width=3 by aaa_inv_zero_aux/ qed-.
+
+fact aaa_inv_lref_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀i. T = #(⫯i) →
+ ∃∃I,K,V. L = K.ⓑ{I}V & ⦃G, K⦄ ⊢ #i ⁝ A.