λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / i_dynamic / ntas_cpcs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_cpcs.ma
index 8438e030746076a61b6b0be1eca4188e4cd8544c..6adb6f7adedaad1d407e2eb131e2a8dabd4e6b28 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_cpcs.ma
@@ -32,5 +32,5 @@ lemma ntas_inv_zero (h) (a) (G) (L):
       ∀T1,T2. ⦃G,L⦄ ⊢ T1 :*[h,a,0] T2 →
       ∧∧ ⦃G,L⦄ ⊢ T1 ![h,a] & ⦃G,L⦄ ⊢ T2 ![h,a] & ⦃G,L⦄ ⊢ T1 ⬌*[h] T2.
 #h #a #G #L #T1 #T2 * #T0 #HT1 #HT2 #HT20 #HT10
-/3 width=3 by cprs_div, and3_intro/ 
+/3 width=3 by cprs_div, and3_intro/
 qed-.