X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fpullback.ma;h=81e319e0bd33eb3e7d22b509fdaa5fd69b2de28f;hb=b367de0252e88d6b0476648d5ceac7e4aeffca27;hp=d224e6b0e25b1442085ed5dadea99a8e2a4b637f;hpb=dc71aab016c7d379e82eea08c4425ab763c593ac;p=helm.git

diff --git a/helm/software/matita/tests/pullback.ma b/helm/software/matita/tests/pullback.ma
index d224e6b0e..81e319e0b 100644
--- a/helm/software/matita/tests/pullback.ma
+++ b/helm/software/matita/tests/pullback.ma
@@ -1,26 +1,37 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
+
+(*
+axiom A : Type.
+axiom B : Type.
+axiom B1 : Type.
+axiom C : Type.
+
+axiom f1 : A → B.
+axiom f2 : A → B1.
+axiom f3 : B → C.
+axiom f4 : B1 → C.
+
+coercion f1.
+coercion f2.
+coercion f3.
+coercion f4.
+
+
+
+
+axiom P : Prop.
+
+lemma x : P.
+*)
 
 include "logic/equality.ma".
 
 record L : Type \def {
-  l_c :> Prop;
+  l_c : Prop;
   l_op : l_c \to l_c \to l_c
 }.
 
 record R : Type \def {
-  r_c :> Prop;
+  r_c : Prop;
   r_op : r_c \to r_c \to r_c
 }.
 
@@ -32,19 +43,49 @@ record LR_ : Type \def {
 
 lemma lr_R : LR_ \to R.
 intros;constructor 1;
-[apply rule (lr_L l)
+[apply rule (l_c (lr_L l))
 |rewrite < (lr_w l);apply (r_op (lr_R_ l));]
 qed.
 
+(*
+axiom F : Prop → Prop.
+axiom C : Prop → Prop. 
+
+axiom daemon : ∀x.F x = C x.
+
+lemma xxx : ∀x.F x = C x. apply daemon; qed.
+
+axiom yyyy : ∀x.C (C x) = C (C x) → F (F x) = F (F x).
+
+coercion yyyy. 
+
+lemma x : ∀x. (λy:F (F x) = F (F x).True) (refl_eq ? (C (C x))).
+
+include "nat/factorial.ma".
+lemma xxx : 8! = 8 * 7!. intros; reflexivity; qed.
+
+lemma x : (λy:8!=8!.True) (refl_eq ? (8 * 7!)).
+apply (refl_eq ??);
+*)
+
+(*
 lemma xxx : \forall x. r_c (lr_R x) = l_c (lr_L x).
 intros; reflexivity;
 qed.
+*)
 
-coercion lr_L.
 
 
+definition Prop_OR_LR_1 : LR_ → Prop.
+apply (λx.r_c (lr_R x)).
+qed.
 
+(*
+coercion Prop_OR_LR_1.
 coercion lr_R.
+*)
+
+unification hint (\forall x. r_c (lr_R x) = l_c (lr_L x)).
 
 lemma foo : \forall x,y.l_op ? x (r_op ? x y) = x.