X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv.ma;h=c3fa8e11bcb9000d92c76518604cf109360f305a;hp=92b22a46a39b2f211f688866eb6de824076032ba;hb=5c92c318030a05c766b3f6070dbd23589cbdee04;hpb=e9b09b14538f770b9e65083c24e3e9cf487df648

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
index 92b22a46a..c3fa8e11b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
@@ -13,6 +13,8 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/exclaim_5.ma".
+include "basic_2/notation/relations/exclaim_4.ma".
+include "basic_2/notation/relations/exclaimstar_4.ma".
 include "basic_2/rt_computation/cpms.ma".
 
 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
@@ -33,6 +35,12 @@ inductive cnv (a) (h): relation3 genv lenv term ≝
 interpretation "context-sensitive native validity (term)"
    'Exclaim a h G L T = (cnv a h G L T).
 
+interpretation "context-sensitive restricted native validity (term)"
+   'Exclaim h G L T = (cnv true h G L T).
+
+interpretation "context-sensitive extended native validity (term)"
+   'ExclaimStar h G L T = (cnv false h G L T).
+
 (* Basic inversion lemmas ***************************************************)
 
 fact cnv_inv_zero_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → X = #0 →