cs_proof : is_CSetoid cs_crr cs_eq cs_ap}.
interpretation "setoid equality"
- 'eq x y = (cic:/matita/algebra/CoRN/Setoid/cs_eq.con _ x y).
+ 'eq x y = (cic:/matita/algebra/CoRN/Setoids/cs_eq.con _ x y).
interpretation "setoid apart"
- 'neq x y = (cic:/matita/algebra/CoRN/Setoid/cs_ap.con _ x y).
+ 'neq x y = (cic:/matita/algebra/CoRN/Setoids/cs_ap.con _ x y).
(* visto che sia "ap" che "eq" vanno in Prop e data la "tight-apartness",
"cs_neq" e "ap" non sono la stessa cosa? *)
generalize in match (ap_symmetric S y x). intro.
elim H1. clear H1.
elim H2. clear H2.
-apply H1. unfold. intro. auto.
+apply H1. unfold. intro. autobatch.
qed.
*)
lemma eq_transitive : \forall S : CSetoid. transitive S (cs_eq S).
lemma eq_wdl : \forall S:CSetoid. \forall x,y,z:S. x = y \to x = z \to z = y.
intros.
-(* perche' auto non arriva in fondo ??? *)
+(* perche' autobatch non arriva in fondo ??? *)
apply (eq_transitive_unfolded ? ? x).
apply eq_symmetric_unfolded.
exact H1.
intro x; intros y H H0.
elim (csp'_strext P x y H).
-auto.
+autobatch.
intro H1.
elimtype False.
intro H1.
elim (H1 H0).
-auto.
+autobatch.
intro H3.
elim H3; intro H4.
-auto.
+autobatch.
elim (ap_irreflexive _ _ H4).
Qed.
generalize (H x x y1 y2 H0); intro H1.
elim H1; intro H2.
-auto.
+autobatch.
elim H2; intro H3.
elim (ap_irreflexive _ _ H3).
-auto.
+autobatch.
Qed.
Lemma Crel_strextarg_imp_strext :
Crel_strext_rht -> Crel_strext_lft -> Crel_strext.
unfold Crel_strext, Crel_strext_lft, Crel_strext_rht in |- *;
intros H H0 x1 x2 y1 y2 H1.
-elim (H x1 y1 y2 H1); auto.
+elim (H x1 y1 y2 H1); autobatch.
intro H2.
-elim (H0 x1 x2 y2 H2); auto.
+elim (H0 x1 x2 y2 H2); autobatch.
Qed.
*)
red in |- *; intros x y z H H0.
elim (Ccsr_strext R x x y z H).
-auto.
+autobatch.
intro H1; elimtype False.
elim H1; intro H2.
red in |- *; intros x y z H H0.
elim (Ccsr_strext R x z y y H).
-auto.
+autobatch.
intro H1; elimtype False.
elim H1; intro H2.
red in |- *; intros x1 x2 y1 y2 H.
case (ap_cotransitive_unfolded _ _ _ H x2); intro H0.
-auto.
+autobatch.
case (ap_cotransitive_unfolded _ _ _ H0 y2); intro H1.
-auto.
+autobatch.
right; right.
apply ap_symmetric_unfolded.
definition un_op_fun: \forall S:CSetoid. CSetoid_un_op S \to CSetoid_fun S S
\def \lambda S.\lambda f.f.
-coercion cic:/matita/algebra/CoRN/Setoid/un_op_fun.con.
+coercion cic:/matita/algebra/CoRN/Setoids/un_op_fun.con.
definition cs_un_op_strext : \forall S:CSetoid. \forall f: CSetoid_fun S S. fun_strext S S (csf_fun S S f) \def
\lambda S:CSetoid. \lambda f : CSetoid_fun S S. csf_strext S S f.
definition bin_op_bin_fun: \forall S:CSetoid. CSetoid_bin_op S \to CSetoid_bin_fun S S S
\def \lambda S.\lambda f.f.
-coercion cic:/matita/algebra/CoRN/Setoid/bin_op_bin_fun.con.
+coercion cic:/matita/algebra/CoRN/Setoids/bin_op_bin_fun.con.
CSetoid_outer_op S S \to CSetoid_bin_fun S S S
\def \lambda S.\lambda f.f.
-coercion cic:/matita/algebra/CoRN/Setoid/outer_op_bin_fun.con.
+coercion cic:/matita/algebra/CoRN/Setoids/outer_op_bin_fun.con.
(* begin hide
Identity Coercion outer_op_bin_fun : CSetoid_outer_op >-> CSetoid_bin_fun.
end hide *)
apply eq_symmetric_unfolded.assumption.
apply eq_symmetric_unfolded.assumption.
apply H.
-auto new.
+autobatch new.
qed.
(*