set "baseuri" "cic:/matita/technicalities/setoids".
include "datatypes/constructors.ma".
-include "logic/connectives2.ma".
include "logic/coimplication.ma".
+include "logic/connectives2.ma".
(* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
Morphism_Theory In' Out'.
intros;
apply (mk_Morphism_Theory ? ? f);
- unfold In' in f; clear In';
- unfold Out' in f; clear Out';
+ unfold In' in f ⊢ %; clear In';
+ unfold Out' in f ⊢ %; clear Out';
generalize in match f; clear f;
elim In;
[ unfold make_compatibility_goal;
apply mk_Morphism_Theory;
[ exact Aeq
| unfold make_compatibility_goal;
- simplify;
+ simplify; unfold ASetoidClass; simplify;
intros;
split;
unfold transitive in H;
(Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) Iff_Relation_Class).
intros;
apply mk_Morphism_Theory;
- reduce;
+ normalize;
[ exact Aeq
| intros;
split;
apply mk_Morphism_Theory;
[ simplify;
apply Aeq
- | simplify;
+ | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify;
intros;
whd;
intros;
apply mk_Morphism_Theory;
[ simplify;
apply Aeq
- | simplify;
+ | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify;
intros;
whd;
intro;
| generalize in match f; clear f;
unfold In'; clear In';
elim In;
- [ reduce;
+ [ normalize;
intro;
apply iff_refl
| simplify;
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));
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));
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
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