Unified refactoring

[helm.git] / matita / contribs / prova.ma

diff --git a/matita/contribs/prova.ma b/matita/contribs/prova.ma
index 7751a0d1f62476d90a4241d96f1c5d8c87a2fc1d..a2012b12f2ca6a18ee633d6d68c3861fd7442d4d 100644 (file)
--- a/matita/contribs/prova.ma
+++ b/matita/contribs/prova.ma
@@ -12,9 +12,29 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/tests".
+set "baseuri" "cic:/matita/test/prova".
 
-include "../contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma".
+include "../contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma".
+
+alias id "Abst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/2)".
+alias id "Abbr" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/1)".
+(*
+alias id "B" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1)".
+*)
+theorem not_abbr_abst:
+ (Abbr\neq Abst)
+.(* tactics: 7 *)
+whd in \vdash (%).
+intros 1 (H).
+letin DEFINED \def (\lambda ee:B
+ .match ee in B return \lambda _:B.Prop with 
+  [Abbr\rArr True|Abst\rArr False|Void\rArr False]).(* extracted *)
+cut (DEFINED Abbr) as ASSUMED;
+[rewrite > H in ASSUMED:(%) as (H0)
+|apply I
+].
+elim H0 using False_ind names 0.(* 2 C I 2 0 *)
+qed.
 
 alias id "Abbr" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/1)".
 alias id "Abst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/2)".
@@ -51,3 +71,10 @@ alias id "THead" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/T.ind#xp
 
 inline procedural
    "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con".
+(*
+inline procedural
+   "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/pr3/ty3_sred_wcpr0_pr0.con".
+
+inline procedural
+   "cic:/Coq/Reals/RiemannInt/FTC_Riemann.con".
+*)