proposition: Lemma option_fmap_inj {A B} (R1 : A → A → Prop) (R2 : B → B → Prop) (f : A → B) : Inj R1 R2 f → Inj (option_Forall2 R1) (option_Forall2 R2) (fmap f).
proof: Proof. intros ? [?|] [?|]; inv 1; constructor; auto. Qed.
imports: stdpp(options)