proposition: Lemma op_if A B (b : bool) (vS vN : option A) (vS1 : A -> B) (vN1 : B) : (if (if b then vS else vN) is Some v then vS1 v else vN1) = if b then if vS is Some v then vS1 v else vN1 else if vN is Some v then vS1 v else vN1.
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)