proposition: Lemma option_rect_function {A B C S' N' v} f : f (option_rect (fun _ : option A => option B) S' N' v) = option_rect (fun _ : option A => C) (fun x => f (S' x)) (f N') v.
proof: Proof. destruct v; reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.Relations.Relation_Definitions Fiat.Common.Coq__8_4__8_5__Compat