proposition: Theorem Diagram : forall (v:A) (u1:R v x) (u2:star _ R z v), coherence y z.
proof: Proof. intros v u1 u2. assert (H:=Hyp2 x u v t1 u1). induction H as [w [s1 s2]]. assert (H':=(hyp_ind u t1 y w t2 s1)). induction H' as [a [v1 v2]]. assert (H'':=(hyp_ind v u1 a z (star_trans _ _ a w v v2 s2) u2)). induction H'' as [b [w1 w2]]. apply coherence_intro with b. apply star_trans with a;assumption. assumption. Qed.
imports: CoLoR(weaved_relation closure terminaison)