順序
Require Import Utf8 Classical.
Example hansya U R:=
forall a:U,R a a:Prop.
Example hihansya U R:=
forall a:U,~R a a:Prop.
Example hantaisyo U R:=
forall a b:U,R a b->R b a->a=b:Prop.
Example sui U(R:U->U->Prop):=
forall a b c,R a b->R b c->R a c.
Example hikakukano U R:=
forall a b:U,R a b\/R b a:Prop.
Example hitaisyo U(R:U->U->Prop):=
forall a b,R a b->~R b a.
Goal forall U(R1 R2:U->U->Prop),
hantaisyo U R1->
(forall a b,R2 a b->R1 a b/\a<>b)->
hitaisyo U R2.
intros.
unfold hitaisyo.
intros.
intro.
assert(H3:=H0 a b).
specialize(H0 b a).
specialize(H0 H2).
clear H2.
specialize(H3 H1).
clear H1 R2.
destruct H0,H3.
apply H3.
clear H1 H3.
unfold hantaisyo in H.
specialize(H a b).
specialize(H H2 H0).
clear R1 H0 H2.
case H.
clear b H.
reflexivity.
Qed.
Goal forall U(R1 R2:U->U->Prop),
sui U R1->
hantaisyo U R1->
(forall a b,R2 a b<->R1 a b/\a<>b)->
sui U R2.
intros.
unfold sui.
intros.
assert(H4:=H1 a b).
assert(H5:=H1 b c).
specialize(H1 a c).
destruct H1,H4,H5.
clear H1 H7 H8.
apply H6.
clear H6.
specialize(H4 H2).
clear H2.
specialize(H5 H3).
clear H3 R2.
destruct H4,H5.
clear H2.
unfold sui in H.
specialize(H a b c).
specialize(H H1 H3).
unfold hantaisyo in H0.
specialize(H0 a b).
split.
clear b H0 H1 H3 H4.
assumption.
clear H.
intro.
apply H4.
clear H4.
subst.
specialize(H0 H1 H3).
clear R1 H1 H3.
case H0.
clear b H0.
reflexivity.
Qed.
Goal forall U(R1 R2:U->U->Prop),
(forall a b,R2 a b->R1 a b/\a<>b)->
hihansya U R2.
intros.
unfold hihansya.
intros.
intro.
specialize(H a a).
specialize(H H0).
clear H0 R2.
destruct H.
clear R1 H.
apply H0.
clear H0.
reflexivity.
Qed.
Goal forall U(R1 R2:U->U->Prop),
(forall a b,R1 a b\/a=b->R2 a b)->
hansya U R2.
intros.
unfold hansya.
intro.
specialize(H a a).
apply H.
clear R2 H.
right.
clear R1.
reflexivity.
Qed.
