update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / nta / nta_sta.etc

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 6268b98b1a9a3cbdcf704eb4f256942be8c91010..b465eab414b850577526ae17717b3da427de0938 100644 (file)
--- 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).
+*)