X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2Fesempio.ma;h=8f9604a8524817acdbc1489a7613b43239981310;hb=d35aca0e979a9c7edbc60c44040360d52be8ca82;hp=d0f6a2e8692f5c64d84ef44779817dfb733af925;hpb=68e7533f986352a86ea0288909b27f83d44893a6;p=helm.git

diff --git a/helm/software/components/ng_refiner/esempio.ma b/helm/software/components/ng_refiner/esempio.ma
index d0f6a2e86..8f9604a85 100644
--- a/helm/software/components/ng_refiner/esempio.ma
+++ b/helm/software/components/ng_refiner/esempio.ma
@@ -17,6 +17,13 @@ include "nat/plus.ma".
 definition hole : ∀A:Type.A → A ≝ λA.λx.x.
 definition id : ∀A:Type.A → A ≝ λA.λx.x.
 
+(* Common case in dama, reduction with metas
+inductive list : Type := nil : list | cons : nat -> list -> list.
+let rec len l := match l with [ nil => O | cons _ l => S (len l) ].
+axiom lt : nat -> nat -> Prop.
+axiom foo : ∀x. Not (lt (hole ? x) (hole ? O)) = (lt x (len nil) -> False).
+*) 
+
 (* meta1 Vs meta2 with different contexts
 axiom foo: 
   ∀P:Type.∀f:P→P→Prop.∀x:P.
@@ -49,7 +56,7 @@ axiom foo:
 *)  
    
 alias num (instance 0) = "natural number".
-axiom foo: (12+12) = (12+11).
+axiom foo: (100+111) = (100+110). 
 
 
     (id ?(id ?(id ?(id ? (100+100))))) =