X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fnta%2Fnta_sta.etc;h=b465eab414b850577526ae17717b3da427de0938;hb=e0c91d8a4422da0b39aca790e5826dc8a617b303;hp=6268b98b1a9a3cbdcf704eb4f256942be8c91010;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_sta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_sta.etc
index 6268b98b1..b465eab41 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_sta.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_sta.etc
@@ -40,3 +40,7 @@ lemma nta_fwd_sta: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U →
   lapply (cpcs_trans … HU01 … HU12) -U1 /2 width=3/
 ]
 qed-.
+(*
+      Lemma ty3_sty0: (g:?; c:?; u,t1:?) (ty3 g c u t1) ->
+                      (t2:?) (sty0 g c u t2) -> (ty3 g c u t2).
+*)