From ce3c2e0c887e0f8303ae9c15e22bc7e29bb89462 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Apr 2008 11:01:53 +0000 Subject: [PATCH] more fix removed from types in proofs --- helm/software/matita/library/technicalities/setoids.ma | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma index 36bea989e..78b58ba31 100644 --- a/helm/software/matita/library/technicalities/setoids.ma +++ b/helm/software/matita/library/technicalities/setoids.ma @@ -694,9 +694,10 @@ theorem apply_morphism_compatibility_Right2Left: 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 Right2Left n t2 t4); elim H2; clear H2; - change in H4 with - (relation_of_product_of_arguments Right2Left n t2 t4); change with (relation_of_relation_class unit Out (apply_morphism n Out (m1 t3) t4) (apply_morphism n Out (m2 t1) t2)); @@ -898,7 +899,7 @@ definition interp : rewrite < (about_carrier_of_relation_class_and_relation_class_of_argument_class S); exact c1 - | split; + | simplify;split; [ rewrite < (about_carrier_of_relation_class_and_relation_class_of_argument_class S); exact c1 -- 2.39.2