qed.
-(* Questa coercion composta non e' stata generata automaticamente *)
+(* Questa coercion composta non e' stata generata autobatchmaticamente *)
lemma mycor: ∀S. CSetoid_bin_op S → (S → S → S).
intros;
unfold in c;
letin H40 \def (csf_strext A B g).
unfold in H40.
elim (H10 (csf_fun ? ? g x1) (csf_fun ? ? g x2) (csf_fun ? ? g y1) (csf_fun ? ? g y2) H0);
-[left | right]; auto.
+[left | right]; autobatch.
qed.
definition compose_CSetoid_bin_fun: \forall A, B, C : CSetoid.
intro.
unfold in H.
apply False_ind.
-apply H1.apply t.
+apply H1.apply a.
exact H2|exact H2]
]
qed.
right. apply I|intros (a at).simplify. left. apply I]]
simplify.
left.
-auto new|intros 2 (c l).
+autobatch |intros 2 (c l).
intros 2 (Hy).
elim y 0[
intros 2 (H z).
elim x 0[
intro y.
elim y 0[
- split[simplify.intro.auto new|simplify.intros.exact H1]|
+ split[simplify.intro.autobatch|simplify.intros.exact H1]|
intros (a at).
simplify.
-split[intro.auto new|intros. exact H1]
+split[intro.autobatch|intros. exact H1]
]
|
intros (a at IHx).
elim y 0[simplify.
- split[intro.auto new|intros.exact H]
+ split[intro.autobatch|intros.exact H]
|
intros 2 (c l).
generalize in match (IHx l).
unfold pred_wd.
unfold conjP.
intros.elim c.
- split [ apply (f x ? t).assumption|apply (f1 x ? t1). assumption]
+ split [ apply (f x ? a).assumption|apply (f1 x ? b). assumption]
qed.
(* End Conjunction. *)
intros.
elim e.
apply (existT).assumption.
-apply (t1 t).
+apply (b a).
qed.
(*
unfold.
intros (x y H1 H2).
elim H1;split[apply (H x).assumption. exact H2|
- intro H5.apply (H0 x ? t)[apply H2|apply t1]
+ intro H5.apply (H0 x ? a)[apply H2|apply b]
]
qed.
exact (eq_imp_not_ap ? ? ? H).
qed.
-(* Similar for automorphisms. *)
+(* Similar for autobatchmorphisms. *)
record PartFunct (S : CSetoid) : Type \def
{pfdom : S -> Type;
intros.
generalize in match (ap_cotransitive_unfolded ? ? ? H1 a).
intro.elim H2.apply False_ind.apply (eq_imp_not_ap ? ? ? H).
-auto.assumption.
+apply ap_symmetric_unfolded. assumption.
+assumption.
qed.
lemma Dir_bij : \forall A, B:CSetoid.
apply (eq_to_ap_to_ap ? ? ? ? (H1 ?)).
apply ap_symmetric_unfolded.assumption
|unfold surjective.intros.
- elim f.auto.
+ elim f.autobatch.
]
qed.
bijective ? ? (inverse A B f).
intros;
elim f 2;
- elim c2 0;
- elim c3 0;
+ elim c 0;
+ elim c1 0;
simplify;
intros;
split;
apply ap_symmetric_unfolded.
apply (eq_to_ap_to_ap ? ? ? ? (H3 ?)).
apply ap_symmetric_unfolded.assumption|
- intros.auto]
+ intros.autobatch]
qed.
(* End bijections.*)