claudio, please have a look at this

diff --git a/helm/software/matita/tests/ng_coercions.ma b/helm/software/matita/tests/ng_coercions.ma
index 1a16862670a8b6fa809a8517ac38df4a657881aa..308697d3c7d1cefd3a73b903755067d217858f13 100644 (file)
--- a/helm/software/matita/tests/ng_coercions.ma
+++ b/helm/software/matita/tests/ng_coercions.ma
@@ -12,19 +12,31 @@
 (*                                                                        *)
 (**************************************************************************)
 
-axiom A : Type.
-axiom B : Type.
-axiom C : Type.
+include "ng_pts.ma".
 
-axiom f : A → B.
-axiom g : B → C.
+ninductive list (A : Type) : Type ≝ 
+ | nil : list A
+ | cons : A → list A → list A. 
 
-(* nlemma xxx : ∀P:C → Prop. ∀x:A. P x. *)  
+naxiom T : Type.
+naxiom S : Type.
+naxiom c : list T → list S.
 
-coercion f. coercion g.
+ncoercion foo : ∀_l:list T. list S ≝ c    
+  on _l : list T 
+  to      list ?.
+  
+naxiom P : list S → Prop.  
+  
+ndefinition t1 ≝ ∀x:list T.P x → ?. ##[ napply Prop; ##] nqed.
+  
+ncoercion bar : ∀_l:list T. S → S ≝ λ_.λx.x     
+  on _l : list T 
+  to      Π_.?.
+  
+naxiom Q : (S → S) → Prop.
 
-axiom T : Type.
+ndefinition t2 ≝ ∀x:list T.Q x → ?. ##[ napply Prop; ##] nqed.
 
-axiom h : A → T. coercion h. 
-
-nlemma xxx : ∀P:C → Prop. ∀x:A. P x.  
\ No newline at end of file
+  
+  
\ No newline at end of file