proposition: Theorem OTP_inf_th_sec_r : forall (x : T), comp_spec eq RndT (r <-$ RndT; ret (T_op r x)).
proof: Proof. intros. eapply (@comp_spec_eq_trans_l _ _ _ _ RndT (x <-$ RndT; ret x)). eapply comp_spec_eq_symm. eapply comp_spec_right_ident. eapply comp_spec_seq. trivial. trivial. eapply comp_spec_symm. eapply (comp_spec_iso (fun b => T_op b x) (fun b => T_op b (T_inverse x))); intuition. rewrite op_assoc. rewrite inverse_l_ident. eauto. rewrite op_assoc. rewrite inverse_r_ident. eauto. eapply all_in_support; eauto. intuition. subst. eapply comp_spec_eq_refl. Qed.
imports: FCF.FCF