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