update in apps_2

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

(* Note: sort evaluation *)
   sv: nat → dd;

(* Note: interpretation: sort *)
   ms: ∀gv,lv,s. ⟦⋆s⟧{M}[gv, lv] ≗ sv M s;