update in apps_2

[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / etc / models / model.etc

diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model.etc
index 51ea8d85bc10eccd379ff0cc590f488363a7e06b..98f74ff5086df202c230c209ed3c70979f6bacdf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model.etc
+++ b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model.etc
@@ -1,7 +1,6 @@
 
-lemma pippo: ∀M,v1,v2,d,i. [i⬐d] v1 ≐⦋M⦌ v2 → v1 ≐⦋M⦌ ↓[i,1] v2.
-#M #v1 #v2 #d #i #H #j elim (lt_or_ge … j i) #Hij
-[ >lower_lt // <(H j) >raise_lt //
-| >lower_ge // <(H (j+1)) >raise_gt /2 width=1 by le_S_S/
-]
-qed-.
+(* Note: sort evaluation *)
+   sv: nat → dd;
+
+(* Note: interpretation: sort *)
+   ms: ∀gv,lv,s. ⟦⋆s⟧{M}[gv, lv] ≗ sv M s;