milestone update in ground_2 and basic_2A

[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / computation / csx_vector.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/computation/csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2A/computation/csx_vector.ma
index b45bc8b5e4b4ee85014e8d3463f4ffceb55d9e10..43391ecfadcb7207a52e758243c78f0c9c9ddb60 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2A/computation/csx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/computation/csx_vector.ma
@@ -26,7 +26,7 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma csxv_inv_cons: ∀h,g,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬊*[h, g] T @ Ts →
+lemma csxv_inv_cons: ∀h,g,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬊*[h, g] T ⨮ Ts →
                      ⦃G, L⦄ ⊢ ⬊*[h, g] T ∧ ⦃G, L⦄ ⊢ ⬊*[h, g] Ts.
 normalize // qed-.