proposition: Lemma fun_op A B C (b : option A) (vS : A -> B) (vN : B) (f : B -> C) : f (if b is Some v then vS v else vN) = if b is Some v then f (vS v) else f vN.
proof: Proof. by case: b=>//. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)