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;
unfold symmetric in sym;
intro;
- autobatch new
+ [ apply (H x2 x1 x3 ? ?);
+ [apply (sym x1 x2 ?).
+ apply (H1).
+ |apply (H x1 x x3 ? ?);
+ [apply (H3).
+ |apply (H2).
+ ]
+ ]
+ | apply (H x1 x3 x ? ?);
+ [apply (H x1 x2 x3 ? ?);
+ [apply (H1).
+ |apply (H3).
+ ]
+ |apply (sym x x3 ?).
+ apply (H2).
+ ]
+ ]
].
qed.
(Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) Iff_Relation_Class).
intros;
apply mk_Morphism_Theory;
- reduce;
+ normalize;
[ exact Aeq
| intros;
split;
intro;
unfold transitive in H;
unfold symmetric in sym;
- autobatch depth=4.
+ [ apply (H x2 x1 x3 ? ?);
+ [apply (sym x1 x2 ?).
+ apply (H1).
+ |apply (H x1 x x3 ? ?);
+ [apply (H3).
+ |apply (H2).
+ ]
+ ]
+ | apply (H x1 x2 x ? ?);
+ [apply (H1).
+ |apply (H x2 x3 x ? ?);
+ [apply (H3).
+ |apply (sym x x3 ?).
+ apply (H x x3 x3 ? ?);
+ [apply (H2).
+ |apply (refl x3).
+ ]
+ ]
+ ]
+ ]
]
qed.
apply mk_Morphism_Theory;
[ simplify;
apply Aeq
- | simplify;
+ | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify;
intros;
whd;
intros;
- autobatch
+ apply (H x2 x1 x3 ? ?);
+ [apply (H1).
+ |apply (H x1 x x3 ? ?);
+ [apply (H3).
+ |apply (H2).
+ ]
+ ]
].
qed.
apply mk_Morphism_Theory;
[ simplify;
apply Aeq
- | simplify;
+ | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify;
intros;
whd;
intro;
- autobatch
+ apply (H x2 x1 x3 ? ?);
+ [apply (H1).
+ |apply (H x1 x x3 ? ?);
+ [apply (H3).
+ |apply (H2).
+ ]
+ ]
].
qed.
| generalize in match f; clear f;
unfold In'; clear In';
elim In;
- [ reduce;
+ [ normalize;
intro;
apply iff_refl
| simplify;
whd;
unfold impl;
intros;
+ apply (H1 ?).apply (H ?).apply (H2).
autobatch.
qed.