Library rel


Inductive compose1 (A B C:Set) (g:B->C->Prop) (f:A->B->Prop) (a:A) (c:C) : Prop :=

 compose1_def : forall b, 

               f a b -> g b c -> (compose1 A B C g f a c).

Implicit Arguments compose1 [A B C].

Inductive compose2 (A B C D:Set) (h:B->C->D->Prop) (f:A->B->Prop) (g:A->C->Prop) (a:A) (d:D) : Prop :=

 compose2_def : forall b c, 

               f a b -> g a c -> h  b c d -> (compose2 A B C D h f g a d).

Implicit Arguments compose2 [A B C D].

Inductive compose3 (A B C D E:Set) (h:B->C->D->E->Prop) (f1:A->B->Prop) (f2:A->C->Prop) (f3:A->D->Prop) (a:A) (e:E) : Prop :=

 compose3_def : forall b c d, 

               f1 a b -> f2 a c -> f3 a d -> h b c d e -> (compose3 A B C D E h f1 f2 f3 a e).

Implicit Arguments compose3 [A B C D E].




Inductive const (A B:Set) (b:B): A -> B -> Prop :=

 const_def : forall a, const A B b a b.

Implicit Arguments const [B].




Inductive pos1of3 (A B C:Set) : A*B*C->A->Prop :=

 pos1of3_def : forall a b c, pos1of3 A B C (a,b,c) a.

Implicit Arguments pos1of3 [A B C].

Inductive pos2of3 (A B C:Set) : A*B*C->B->Prop :=

 pos2of3_def : forall a b c, pos2of3 A B C (a,b,c) b.

Implicit Arguments pos2of3 [A B C].

Inductive pos3of3 (A B C:Set) : A*B*C->C->Prop :=

 pos3of3_def : forall a b c, pos3of3 A B C (a,b,c) c.

Implicit Arguments pos3of3 [A B C].
Index
This page has been generated by coqdoc