proposition: Lemma fold_option_rect_nodep {A B} (S : A -> B) (N : B) (v : option A) : match v return B with | Some x => S x | None => N end = option_rect_nodep S N v.
proof: Proof. reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.Relations.Relation_Definitions Fiat.Common.Coq__8_4__8_5__Compat