X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprova.ma;h=a2012b12f2ca6a18ee633d6d68c3861fd7442d4d;hb=e465656be7e67ee3c02acf12a53c8388ae384b0a;hp=a3357f8e0d62f977e059418a4cbad07f21384c44;hpb=3ce05ecd50428a27ce17adb070620aeeaf2aed65;p=helm.git

diff --git a/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma
index a3357f8e0..a2012b12f 100644
--- a/helm/software/matita/contribs/prova.ma
+++ b/helm/software/matita/contribs/prova.ma
@@ -16,6 +16,26 @@ set "baseuri" "cic:/matita/test/prova".
 
 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)".
 alias id "Appl" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/F.ind#xpointer(1/1/1)".