still more additions and corrections for the article

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / nta.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
index 84bbfeda94a2c4df1493e9833e525707ee2134a7..187370fab65a16de7c9c9d0c489a272a3733f56e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
@@ -78,14 +78,14 @@ qed-.
 (* Basic_forward lemmas *****************************************************)
 
 lemma nta_fwd_cnv_sn (a) (h) (G) (L):
-                     ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ T ![a,h].
+      ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ T ![a,h].
 #a #h #G #L #T #U #H
 elim (cnv_inv_cast … H) -H #X #_ #HT #_ #_ //
 qed-.
 
 (* Note: this is nta_fwd_correct_cnv *)
 lemma nta_fwd_cnv_dx (a) (h) (G) (L):
-                     ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ U ![a,h].
+      ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ U ![a,h].
 #a #h #G #L #T #U #H
 elim (cnv_inv_cast … H) -H #X #HU #_ #_ #_ //
 qed-.