fact csxa_intro_aux: ∀h,g,G,L,T1. (
∀T,T2. ⦃G, L⦄ ⊢ T ➡*[h, g] T2 → T1 = T → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2
) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1.
fact csxa_intro_aux: ∀h,g,G,L,T1. (
∀T,T2. ⦃G, L⦄ ⊢ T ➡*[h, g] T2 → T1 = T → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2
) → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1.