- [ apply basic_pair
- | apply relation_pair_setoid
- | apply id_relation_pair
- | apply relation_pair_composition
- | intros;
+ [ apply relation_pair_composition;
+ | apply relation_pair_composition_is_morphism;]
+qed.
+
+lemma relation_pair_composition_morphism_assoc:
+Πo1:basic_pair
+.Πo2:basic_pair
+ .Πo3:basic_pair
+ .Πo4:basic_pair
+ .Πa12:relation_pair_setoid o1 o2
+ .Πa23:relation_pair_setoid o2 o3
+ .Πa34:relation_pair_setoid o3 o4
+ .relation_pair_composition_morphism o1 o3 o4
+ (relation_pair_composition_morphism o1 o2 o3 a12 a23) a34
+ =relation_pair_composition_morphism o1 o2 o4 a12
+ (relation_pair_composition_morphism o2 o3 o4 a23 a34).
+ intros;