proposition: Lemma option_rect_Proper_nondep_eq {A B} {S S' : A -> B} {N N' v} (HS : forall vv, v = Some vv -> S vv = S' vv) (Hn : v = None -> N = N') : option_rect (fun _ : option A => B) S N v = option_rect (fun _ : option A => B) S' N' v.
proof: Proof. destruct v; simpl; auto using eq_refl with nocore. Qed.
imports: Coq.Classes.Morphisms Coq.Relations.Relation_Definitions Fiat.Common.Coq__8_4__8_5__Compat