...

[helm.git] / helm / software / components / ng_refiner / esempio.ma

diff --git a/helm/software/components/ng_refiner/esempio.ma b/helm/software/components/ng_refiner/esempio.ma
index 4005ee98ac2a187b441f06556473fbfbf3594579..e686e7eeef38c1669e74fe4b415de82c36091f8d 100644 (file)
--- a/helm/software/components/ng_refiner/esempio.ma
+++ b/helm/software/components/ng_refiner/esempio.ma
@@ -16,18 +16,6 @@ include "nat/plus.ma".
 
 definition hole : ∀A:Type.A → A ≝ λA.λx.x.
 
-inductive pippo (T:Type) (x:T) : Prop ≝ . 
-
-axiom A: Type. 
-axiom B:A.
-
-axiom foo : \forall x: (hole ? A).pippo (hole ? A) x.
-
-axiom foo: (λx,y:A. pippo (hole ? A) x y) 
-           (hole ? B) (hole ? B).
-
-axiom foo: λx:(hole ? Type).λy:(hole ? Type). pippo (hole ? Type) x y.
-
 axiom foo: (λx,y.(λz. z x + z (x+y)) (λw:nat.hole ? w)) = λx,y.x. (* KO, delift rels only *) 
 axiom foo: (λx,y.(λz. z (x+y) + z x) (λw:nat.hole ? w)) = λx,y.x. (* OK *)