fact: Definition sum_decode {x y} : sum_code x y -> x = y := match x, y return sum_code x y -> x = y with | inl x', inl y' => @f_equal _ _ (@inl _ _) _ _ | inr x', inr y' => @f_equal _ _ (@inr _ _) _ _ | _, _ => 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