proposition: Lemma transitive_pR : Transitive (pointwise_refine).
proof: Proof. unfold Transitive, pointwise_refine, pointwise_relation; intros. etransitivity. apply H; eauto. apply H0. reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.SetoidTactics Fiat.Computation