λδ site update

[helm.git] / helm / software / matita / tests / pullback.ma

diff --git a/helm/software/matita/tests/pullback.ma b/helm/software/matita/tests/pullback.ma
index 54b784caae96b84d1ea88e9933938f8b1240c450..81e319e0bd33eb3e7d22b509fdaa5fd69b2de28f 100644 (file)
--- a/helm/software/matita/tests/pullback.ma
+++ b/helm/software/matita/tests/pullback.ma
@@ -26,24 +26,24 @@ 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
 }.
 
 record LR_ : Type \def {
-  lr_L :> L ;
+  lr_L : L ;
   lr_R_ : R ;
   lr_w : r_c lr_R_ = l_c lr_L
 }.
 
 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.
 
@@ -80,8 +80,12 @@ 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.