proposition: Lemma option_rect_ext {A P} Ps Ps' Pn Pn' x (Hs : forall k, Ps k = Ps' k) (Hn : Pn = Pn') : @option_rect A P Ps Pn x = @option_rect A P Ps' Pn' x.
proof: Proof. destruct x; simpl; rewrite ?Hs, ?Hn; reflexivity. Defined.
imports: Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Coq.Arith.PeanoNat Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Common