-fact cpy_inv_flat1_aux: ∀d,e,L,U1,U2. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 →
- ∀I,V1,T1. U1 = ⓕ{I} V1. T1 →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶×[d, e] V2 & ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 &
- U2 = ⓕ{I} V2. T2.
-#d #e #L #U1 #U2 * -d -e -L -U1 -U2
-[ #L #k #d #e #I #V1 #T1 #H destruct
-| #L #K #V #W #i #d #e #_ #_ #_ #_ #I #V1 #T1 #H destruct
-| #L #a #J #V1 #V2 #T1 #T2 #d #e #_ #_ #I #V #T #H destruct
-| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #I #V #T #H destruct /2 width=5/
+fact cpy_inv_flat1_aux: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 →
+ ∀I,V1,T1. U1 = ⓕ{I}V1.T1 →
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶×[d, e] V2 &
+ ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 &
+ U2 = ⓕ{I}V2.T2.
+#G #L #U1 #U2 #d #e * -G -L -U1 -U2 -d -e
+[ #I #G #L #d #e #J #W1 #U1 #H destruct
+| #I #G #L #K #V #W #i #d #e #_ #_ #_ #_ #J #W1 #U1 #H destruct
+| #a #I #G #L #V1 #V2 #T1 #T2 #d #e #_ #_ #J #W1 #U1 #H destruct
+| #I #G #L #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/