-fact crf_inv_abst_aux: ∀a,L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓛ{a}W. U →
- L ⊢ 𝐑⦃W⦄ ∨ L.ⓛW ⊢ 𝐑⦃U⦄.
-#a #L #W #U #T * -T
+fact trf_inv_lref_aux: ∀L,T. L ⊢ 𝐑⦃T⦄ → ∀i. T = #i → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
+#L #T * -L -T
+[ #L #K #V #j #HLK #i #H destruct /2 width=3/
+| #L #V #T #_ #i #H destruct
+| #L #V #T #_ #i #H destruct
+| #J #L #V #T #_ #i #H destruct
+| #a #J #L #V #T #_ #_ #i #H destruct
+| #a #J #L #V #T #_ #_ #i #H destruct
+| #a #L #V #W #T #i #H destruct
+| #a #L #V #W #T #i #H destruct
+]
+qed.
+
+lemma trf_inv_lref: ∀L,i. L ⊢ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
+/2 width=3/ qed-.
+
+fact crf_inv_ib2_aux: ∀a,I,L,W,U,T. ib2 a I → L ⊢ 𝐑⦃T⦄ → T = ⓑ{a,I}W. U →
+ L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃U⦄.
+#a #I #L #W #U #T #HI * -T