proposition: Theorem comp_spec_eq_trans_r : forall (A B : Set){eqd : EqDec A}{eqd : EqDec B}(c1 : Comp A)(c2 c3 : Comp B) P, comp_spec P c1 c2 -> comp_spec eq c2 c3 -> comp_spec P c1 c3.
proof: Proof. intuition. destruct H. intuition. exists x. intuition. eapply comp_spec_eq_impl_eq in H0; intuition. rewrite <- H0. trivial. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1