proposition: Lemma Equivalence_optionR : Equivalence_rel R -> Equivalence_rel optionR.
proof: Proof. case/Equivalence_relS=>r s t; apply/Equivalence_relS; split. - by apply: Reflexive_optionR. - by apply: Symmetric_optionR. by apply: Transitive_optionR. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)