The Coq mailing list

[scott constable <sdconsta AT syr.edu>]

Hi All,

I have the following definition of composition:

Inductive Compose : T → V → Prop :=
| comp_intro : ∀ x y z, R1 x y → R2 y z → Compose x z.

Notation "P ∘ R" := (Compose R P) (at level 55, right associativity).

And I am hopelessly lost as to how to prove this theorem:

Lemma compose_assoc : ∀ (R : U → V → Prop) (Q : V → T → Prop)
                          (P : T → W → Prop), P ∘ Q ∘ R = (P ∘ Q) ∘ R.

Any help would be extremely appreciated!

Thanks in advance,

~Scott Constable