From 347b0f483245bd0295f95f99742e23484c331312 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Apr 2008 11:10:12 +0000 Subject: [PATCH] more fix removed from types --- helm/software/matita/library/technicalities/setoids.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma index 78b58ba31..4c51d3a44 100644 --- a/helm/software/matita/library/technicalities/setoids.ma +++ b/helm/software/matita/library/technicalities/setoids.ma @@ -817,9 +817,9 @@ theorem apply_morphism_compatibility_Left2Right: generalize in match H2; clear H2; elim args2 0; clear args2; elim args1; clear args1; + simplify in H2; change in H2:(? ? %) with + (relation_of_product_of_arguments Left2Right n t2 t4); elim H2; clear H2; - change in H4 with - (relation_of_product_of_arguments Left2Right n t2 t4); change with (relation_of_relation_class unit Out (apply_morphism n Out (m1 t1) t2) (apply_morphism n Out (m2 t3) t4)); -- 2.39.2