From d175eb77ca53f7f11377fada4b964ef6c4d0a592 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Dec 2008 10:37:20 +0000 Subject: [PATCH] ... --- helm/software/matita/tests/pullback.ma | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/tests/pullback.ma b/helm/software/matita/tests/pullback.ma index 54b784caa..81e319e0b 100644 --- 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. -- 2.39.2