Some changes to the pullback test, for debugging

diff --git a/helm/software/matita/tests/pullback.ma b/helm/software/matita/tests/pullback.ma
index 1196255d92d3cf39c772cba04ed36a6b05185b94..d224e6b0e25b1442085ed5dadea99a8e2a4b637f 100644 (file)
--- a/helm/software/matita/tests/pullback.ma
+++ b/helm/software/matita/tests/pullback.ma
@@ -12,6 +12,48 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "logic/equality.ma".
+
+record L : Type \def {
+  l_c :> Prop;
+  l_op : l_c \to l_c \to l_c
+}.
+
+record R : Type \def {
+  r_c :> Prop;
+  r_op : r_c \to r_c \to r_c
+}.
+
+record LR_ : Type \def {
+  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)
+|rewrite < (lr_w l);apply (r_op (lr_R_ l));]
+qed.
+
+lemma xxx : \forall x. r_c (lr_R x) = l_c (lr_L x).
+intros; reflexivity;
+qed.
+
+coercion lr_L.
+
+
+
+coercion lr_R.
+
+lemma foo : \forall x,y.l_op ? x (r_op ? x y) = x.
+
+r_c ?1 =?= l_c ?2
+
+
+r_c (lr_R ?3) === l_c (lr_L ?3)
+r_c (lr_R ?) === l_c (lr_L ?)   |---->   
+   \forall x. r_c (lr_R x) === l_c (lr_L x)
 
 
 inductive T : Type \def t : T.