fact: Definition option_decode {x y} : option_code x y -> x = y := match x, y return option_code x y -> x = y with | Some x', Some y' => @f_equal _ _ (@Some _) _ _ | None, None => fun _ => eq_refl | _, _ => fun H => match H : False with end end.
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